Component-wise incremental LTL model checking

DOI10.1007/S00165-015-0347-XzbMath1355.68178OpenAlexW2268613590MaRDI QIDQ510894

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

Publication date: 14 February 2017

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: http://eprints.sztaki.hu/8941/

zbMATH Keywords

symbolic model checkingsaturationincremental algorithmLTLcomponent-wise abstractionSCC computation

Mathematics Subject Classification ID

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

Related Items (1)

Saturation Enhanced with Conditional Locality: Application to Petri Nets

Uses Software

• PNML
• NuSMV
• SPOT
• LTL2BA
• nuXmv

Cites Work

• Symbolic model checking: \(10^{20}\) states and beyond
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Compositional SCC analysis for language emptiness
• Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking
• MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs
• Improving Static Variable Orders Via Invariants
• Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation
• Graph-Based Algorithms for Boolean Function Manipulation
• Lazy abstraction
• Saturation-Based Incremental LTL Model Checking with Inductive Proofs
• Automated Technology for Verification and Analysis
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Depth-First Search and Linear Graph Algorithms
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Component-wise incremental LTL model checking