Skip to content

BDD engine: transform SVA to LTL, then LTL to CTL #1096

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.

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

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

kroening
Copy link
Member

@kroening kroening commented May 2, 2025

The BDD engine now transforms SVA to LTL, when possible, which in turn is transformed to CTL, when possible.

This is strictly more general than the current direct mapping.

@kroening kroening force-pushed the bdd-sva-via-ltl branch from caab4bb to 8da9819 Compare May 2, 2025 21:35
@kroening kroening marked this pull request as ready for review May 2, 2025 21:39
The BDD engine now transforms SVA to LTL, when possible, which in turn is
transformed to CTL, when possible.

This is strictly more general than the current direct mapping.
@kroening kroening force-pushed the bdd-sva-via-ltl branch from 8da9819 to 17fdbb0 Compare May 3, 2025 22:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant