Incremental and complete bounded model checking for full PLTL

DOI10.1007/11513988_10MaRDI QIDQ5716540zbMATH OpenOpenAlexFDO

Authors Keijo Heljanko, Tommi Junttila, Timo Latvala

Publication date 10 January 2006

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

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

zbMATH Keywords

Bounded Model CheckingCompleteIncrementalNuSMVPLTL

Mathematics Subject Classification ID

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

Recommendations

• Simple is better: Efficient bounded model checking for past LTL
• Bounded model checking for past LTL
• Linear Encodings of Bounded LTL Model Checking
• Bounded model checking for propositional projection temporal logic
• Proving more properties with bounded model checking

Cited in

(17)

• Partitioned PLTL model-checking for refined transition systems
• SAT-based explicit LTL reasoning and its application to satisfiability checking
• Linear templates of ACTL formulas with an application to SAT-based verification
• Planning as satisfiability: parallel plans and algorithms for plan search
• Nondeterministic probabilistic Petri net -- a new method to study qualitative and quantitative behaviors of system
• A compact linear translation for bounded model checking
• SAT-Based Model Checking
• scientific article; zbMATH DE number 7445165 (Why is no real title available?)
• Bounded model checking of ETL cooperating with finite and looping automata connectives
• scientific article; zbMATH DE number 1223543 (Why is no real title available?)
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Bounded model checking for past LTL
• Bounded semantics
• Linear Encodings of Bounded LTL Model Checking
• Proving more properties with bounded model checking
• Simple is better: Efficient bounded model checking for past LTL
• SAT meets tableaux for linear temporal logic satisfiability

Describes a project that uses

Uses Software

• SATIRE
• NuSMV
• Chaff
• MiniSat

This page was built for publication: Incremental and complete bounded model checking for full PLTL

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