Bounded model checking for past LTL

MaRDI QIDQ4417910zbMATH OpenFDO

Authors Marco H. Benedetti, Alessandro Cimatti

Publication date 30 July 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2619/26190018.htm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Formal Methods in Computer-Aided Design
• Simple is better: Efficient bounded model checking for past LTL
• Incremental and complete bounded model checking for full PLTL
• Past is for free: on the complexity of verifying linear temporal properties with past
• Past is for free: On the complexity of verifying linear temporal properties with past

Cited in

(13)

• Pardinus: a temporal relational model finder
• Bounded semantics
• Development of global specification for dynamically adaptive software
• Efficient parallel path checking for linear-time temporal logic with past and bounds
• Bounded model checking for propositional projection temporal logic
• On Decidability of LTL+Past Model Checking for Process Rewrite Systems
• Automated Technology for Verification and Analysis
• Formal Methods in Computer-Aided Design
• Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time
• Shortest counterexamples for symbolic model checking of LTL with past
• Simple is better: Efficient bounded model checking for past LTL
• Incremental and complete bounded model checking for full PLTL
• From linear temporal logics to Büchi automata: the early and simple principle

Describes a project that uses

Uses Software

• NuSMV

This page was built for publication: Bounded model checking for past LTL

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