Infinite state model checking by abstract interpretation and program specialisation

DOI10.1007/10720327_5MaRDI QIDQ2723916zbMATH OpenFDO

Authors Michael Leuschel, Thierry Massart

Publication date 8 July 2001

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

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

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• On model checking infinite-state systems
• Abstract logical model checking of infinite-state systems using narrowing
• Model checking abstract state machines and beyond
• scientific article; zbMATH DE number 2102702
• Program specialization for verifying infinite state systems: an experimental evaluation
• Infinite-state invariant checking with IC3 and predicate abstraction
• Bounded model checking of infinite state systems
• Computer Aided Verification
• Symbolic Model Checking of Infinite-State Systems Using Narrowing

Cited in

(15)

• Infinite-state invariant checking with IC3 and predicate abstraction
• Fast offline partial evaluation of logic programs
• Verifying of interface assertions for infinite state Mealy machines
• Incompleteness of states w.r.t. traces in model checking
• State space analysis of Petri nets with relation-algebraic methods
• Program specialization for verifying infinite state systems: an experimental evaluation
• Extending co-logic programs for branching-time model checking
• Analysis of Linear Hybrid Systems in CLP
• scientific article; zbMATH DE number 1744958 (Why is no real title available?)
• Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
• scientific article; zbMATH DE number 2090523 (Why is no real title available?)
• scientific article; zbMATH DE number 7453192 (Why is no real title available?)
• Control-flow refinement by partial evaluation, and its application to termination and cost analysis
• Constraint-based deductive model checking
• Analysis and Transformation of Constrained Horn Clauses for Program Verification

Describes a project that uses

Uses Software

• LOGEN
• XSB
• ECCE

This page was built for publication: Infinite state model checking by abstract interpretation and program specialisation

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