On bounded specifications

DOI10.1007/3-540-45653-8_2zbMATH Open1275.68094OpenAlexW1605190994MaRDI QIDQ2996151FDOQ2996151

Orna Kupferman, Moshe Y. Vardi

Publication date: 6 May 2011

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-45653-8_2

Recommendations

• Bounded model checking for all regular properties
• Bounded model checking for timed automata
• Bounded model checking of infinite state systems
• Linear completeness thresholds for bounded model checking
• Bounded Synthesis

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (9)

• Certifying inexpressibility
• Spanning the spectrum from safety to liveness
• Bounded Synthesis
• Antichains and compositional algorithms for LTL synthesis
• How Much Lookahead is Needed to Win Infinite Games?
• Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
• GSTE is partitioned model checking
• An Automata-Theoretic Approach to Infinite-State Systems
• Temporal Logic and Fair Discrete Systems

This page was built for publication: On bounded specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2996151)