Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Checking traces of Leios execution against the formal specification #143

Open
2 tasks
yveshauser opened this issue Jan 20, 2025 · 0 comments
Open
2 tasks

Checking traces of Leios execution against the formal specification #143

yveshauser opened this issue Jan 20, 2025 · 0 comments
Assignees
@yveshauser
Labels
PI Goal PI-9
Milestone
PI9

Comments

@yveshauser
Copy link
Member

yveshauser commented Jan 20, 2025 •
edited
Loading

  • Define format for execution traces
  • Parse a trace into the representation defined by the semantics of Leios, implicitly constructing required proofs

Acceptance criteria: A trace from a simulation in the specified format is accepted or rejected with respect to the relational model from formal specification
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@yveshauser yveshauser

Labels
PI Goal PI-9
Projects
None yet
Milestone
PI9
Development

No branches or pull requests
2 participants
@yveshauser @will-break-it