Component-wise incremental LTL model checking

DOI10.1007/S00165-015-0347-XzbMATH Open1355.68178OpenAlexW2268613590MaRDI QIDQ510894FDOQ510894

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

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/

Recommendations

• Saturation-based incremental LTL model checking with inductive proofs
• Tools and Algorithms for the Construction and Analysis of Systems
• An explicit transition system construction approach to LTL satisfiability checking
• Tools and Algorithms for the Construction and Analysis of Systems
• MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs

zbMATH Keywords

saturationincremental algorithmLTLsymbolic model checkingcomponent-wise abstractionSCC computation

Mathematics Subject Classification ID

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

Cites Work

• Graph-Based Algorithms for Boolean Function Manipulation
• Depth-First Search and Linear Graph Algorithms
• Symbolic model checking: \(10^{20}\) states and beyond
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Interpolation and SAT-based model checking.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Lazy abstraction
• Symbolic CTL model checking of asynchronous systems using constrained saturation
• Title not available (Why is that?)
• Compositional SCC analysis for language emptiness
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Saturation-Based Incremental LTL Model Checking with Inductive Proofs
• Automated Technology for Verification and Analysis
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems

Cited In (4)

• Bounded rational search for on-the-fly model checking of LTL properties
• Saturation Enhanced with Conditional Locality: Application to Petri Nets
• Tools and Algorithms for the Construction and Analysis of Systems
• Incremental Language Inclusion Checking for Networks of Timed Automata

Uses Software

• PNML
• NuSMV
• SPOT
• LTL2BA
• nuXmv

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

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