Efficient CTL verification via Horn constraints solving

MaRDI QIDQ5015366zbMATH OpenFDO

Authors T. Beyene, Andrey Rybalchenko, C. Popeea

Publication date 7 December 2021

Full work available at URL https://arxiv.org/abs/1607.04456, http://eptcs.web.cse.unsw.edu.au/paper.cgi?HCVS2016.1

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 1799521 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 177234 (Why is no real title available?)
• scientific article; zbMATH DE number 3624762 (Why is no real title available?)
• scientific article; zbMATH DE number 2080197 (Why is no real title available?)
• A compositional approach to CTL\(^*\) verification
• An automata-theoretic approach to branching-time model checking
• Automata, Languages and Programming
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation
• Efficient CTL model-checking for pushdown systems
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• Proving non-termination
• Pushdown model checking for malware detection
• Pushdown processes: Games and model-checking
• State/Event Software Verification for Branching-Time Specifications
• Symbolic model checking: \(10^{20}\) states and beyond
• Temporal property verification as a program analysis task
• Verifying increasingly expressive temporal logics for infinite-state systems

Cited in

(4)

• Leveraging Horn clause solving for compositional verification of PLC software
• On recursion-free Horn clauses and Craig interpolation
• Autark assignments of Horn CNFs
• Verification of time-aware business processes using constrained Horn clauses

Describes a project that uses

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)