Simple is better: Efficient bounded model checking for past LTL

DOI10.1007/978-3-540-30579-8_25MaRDI QIDQ5711503zbMATH OpenOpenAlexFDO

Authors Timo Latvala, Armin Biere, Keijo Heljanko, Tommi Junttila

Publication date 6 December 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b105073

zbMATH Keywords

bounded model checkingNuSMVpast LTL

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Bounded model checking for past LTL
• Formal Methods in Computer-Aided Design
• Incremental and complete bounded model checking for full PLTL
• Linear Encodings of Bounded LTL Model Checking
• Formal Methods in Computer-Aided Design

Cited in

(10)

• Counterexample-preserving reduction for symbolic model checking
• Bounded model checking of ETL cooperating with finite and looping automata connectives
• Bounded model checking for past LTL
• Linear Encodings of Bounded LTL Model Checking
• Automata-Theoretic Model Checking Revisited
• Formal Methods in Computer-Aided Design
• 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
• Incremental and complete bounded model checking for full PLTL

Describes a project that uses

Uses Software

• Chaff
• NuSMV

This page was built for publication: Simple is better: Efficient 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 Q5711503)