Saturation-Based Incremental LTL Model Checking with Inductive Proofs

DOI10.1007/978-3-662-46681-0_58zbMath1420.68135OpenAlexW1884765109MaRDI QIDQ5194964

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

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) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (1)

Component-wise incremental LTL model checking

This page was built for publication: Saturation-Based Incremental LTL Model Checking with Inductive Proofs