scientific article; zbMATH DE number 7440189

zbMath1482.68134arXiv1607.04456MaRDI QIDQ5015366

Tewodros A. Beyene, Andrey Rybalchenko, Corneliu Popeea

Publication date: 7 December 2021

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

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

Related Items (2)

Leveraging Horn clause solving for compositional verification of PLC software ⋮ On recursion-free Horn clauses and Craig interpolation

Uses Software

• YASM
• HSF
• PoMMaDe

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic model checking: \(10^{20}\) states and beyond
• A compositional approach to CTL\(^*\) verification
• Pushdown processes: Games and model-checking
• Temporal property verification as a program analysis task
• Pushdown Model Checking for Malware Detection
• Model-checking CTL* over flat Presburger counter systems
• Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation
• Efficient CTL Model-Checking for Pushdown Systems
• Proving non-termination
• Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
• An automata-theoretic approach to branching-time model checking
• State/Event Software Verification for Branching-Time Specifications
• Automata, Languages and Programming

This page was built for publication: