Saturation-based incremental LTL model checking with inductive proofs

DOI10.1007/978-3-662-46681-0_58MaRDI QIDQ5194964zbMATH OpenOpenAlexFDO

Authors Vince Molnár, Dániel Darvas, András Vörös, Tamás Bartha

Publication date 17 September 2019

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL http://real.mtak.hu/24597/1/TACAS2015_MolnarEtAl.pdf

zbMATH Keywords

model checkinglinear temporal logicstate spaceconcurrent systeminductive proof

Mathematics Subject Classification ID

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)

Recommendations

• Component-wise incremental LTL model checking
• SAT-Based Model Checking without Unrolling
• Computer Aided Verification
• Symbolic CTL model checking of asynchronous systems using constrained saturation
• An explicit transition system construction approach to LTL satisfiability checking

Cited in

(4)

• scientific article; zbMATH DE number 2086516 (Why is no real title available?)
• Computer Aided Verification
• Compositional model checking with incremental counter-example construction
• Component-wise incremental LTL model checking

This page was built for publication: Saturation-based incremental LTL model checking with inductive proofs

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