TOrPEDO : witnessing model correctness with topological proofs

DOI10.1007/s00165-021-00564-1WikidataQ113906134 ScholiaQ113906134MaRDI QIDQ2065548

Claudio Menghi, Anna Bernasconi, Paola Spoletini, Alessandro Maria Rizzi

Publication date: 11 January 2022

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

Full work available at URL: https://doi.org/10.1007/s00165-021-00564-1

zbMATH Keywords

theorem proving; model checking; unsatisfiable core; iterative design; topological proofs

Mathematics Subject Classification ID

68-XX: Computer science

Related Items

TOrPEDO

Uses Software

• BLAST
• NuSMV
• z3
• UFO
• LTSA-WS
• KEGG
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Data structures for symbolic multi-valued model-checking
• Branching-time temporal logic and tree automata
• Multi-robot LTL planning under uncertainty
• Certifying proofs for SAT-based model checking
• Dealing with incompleteness in automata-based model checking
• Supporting verification-driven incremental distributed design of components
• A verification-driven framework for iterative design of controllers
• From Under-Approximations to Over-Approximations and Back
• Linear Completeness Thresholds for Bounded Model Checking
• LTL Generalized Model Checking Revisited
• Integrating Topological Proofs with Model Checking to Instrument Iterative Design
• The Complexity of Linear-Time Temporal Logic Model Repair
• From Model Checking to a Temporal Proof for Partial Models
• Verification: Theory and Practice
• Linear Encodings of Bounded LTL Model Checking
• Automata, Languages and Programming
• CONCUR 2003 - Concurrency Theory
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Formal Approaches to Software Testing