Efficient CTL verification via Horn constraints solving

zbMATH Open1482.68134arXiv1607.04456MaRDI QIDQ5015366FDOQ5015366

Authors: T. Beyene, Andrey Rybalchenko, C. Popeea 

Publication date: 7 December 2021

Full work available at URL: https://arxiv.org/abs/1607.04456

Recommendations

• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Efficient model checking algorithms for computation tree logic and their application to the verification of parallel programs
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Horn clause solvers for program verification
• Verifying increasingly expressive temporal logics for infinite-state systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• Symbolic model checking: \(10^{20}\) states and beyond
• Title not available (Why is that?)
• Title not available (Why is that?)
• Model-checking CTL* over flat Presburger counter systems
• An automata-theoretic approach to branching-time model checking
• Pushdown processes: Games and model-checking
• Pushdown Model Checking for Malware Detection
• Efficient CTL model-checking for pushdown systems
• Title not available (Why is that?)
• A compositional approach to CTL\(^*\) verification
• Automata, Languages and Programming
• Title not available (Why is that?)
• Temporal property verification as a program analysis task
• Proving non-termination
• Title not available (Why is that?)
• Title not available (Why is that?)
• Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
• State/Event Software Verification for Branching-Time Specifications
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation

Cited In (3)

• Autark assignments of Horn CNFs
• On recursion-free Horn clauses and Craig interpolation
• Leveraging Horn clause solving for compositional verification of PLC software

Uses Software

• YASM
• HSF
• PoMMaDe

This page was built for publication: Efficient CTL verification via Horn constraints solving

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