First order Büchi automata and their application to verification of LTL specifications

DOI10.1016/j.jlamp.2024.101021MaRDI QIDQ6643476

Publication date: 26 November 2024

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

zbMATH Keywords

concurrent systems Büchi automata deductive verification linear temporal logics logical methods verification condition generation weak well-founded sets

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

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
Unnamed Item
Unnamed Item
Unnamed Item
Proving termination of nonlinear command sequences
Bounded semantics
Limits of computation. From a programming perspective
Inference of ranking functions for proving temporal properties by abstract interpretation
A new look at the automatic synthesis of linear ranking functions
Expressiveness and the completeness of Hoare's logic
Completeness of Hoare logic with inputs over the standard model
Using branching time temporal logic to synthesize synchronization skeletons
Complexity results for classes of quantificational formulas
Completing the temporal picture
Cut elimination and automatic proof procedures
A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
Depth of proofs, depth of cut-formulas and complexity of cut formulas
On the completeness of propositional Hoare logic
Counter machines
Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
Temporal prophecy for proving temporal properties of infinite-state systems
Linear templates of ACTL formulas with an application to SAT-based verification
Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
The Efficiency of Resolution and Davis--Putnam Procedures
An extension of data automata that captures XPath
Policy Iteration-Based Conditional Termination and Ranking Functions
Two-variable logic on data words
Automatically disproving fair termination of higher-order functional programs
Introduction to Model Checking
Abstraction and Abstraction Refinement
QBF Encoding of Temporal Properties and QBF-Based Verification
Counterexample-guided abstraction refinement for symbolic model checking
Solving SAT and SAT Modulo Theories
An ACL2 Tutorial
XPath satisfiability in the presence of DTDs
An Automata-Theoretic Approach to Infinite-State Systems
Fixpoint-Guided Abstraction Refinements
A proof rule for fair termination of guarded commands
On relative completeness of Hoare logics
Graph-Based Algorithms for Boolean Function Manipulation
Soundness and Completeness of an Axiom System for Program Verification
Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
Short Presburger Arithmetic Is Hard
Finite satisfiability for two‐variable, first‐order logic with one transitive relation is decidable
An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications
Transition predicate abstraction and fair termination
All You Need Is Compassion
Formal Techniques for Networked and Distributed Systems - FORTE 2005
A Machine-Oriented Logic Based on the Resolution Principle
An axiomatic basis for computer programming
A Computing Procedure for Quantification Theory
A machine program for theorem-proving
Theoretical Aspects of Computing - ICTAC 2004
Verification Modulo theories
Alternating automata modulo first order theories
An automata-theoretic approach to linear temporal logic
Formal specification and verification of JDK's identity hash map implementation

This page was built for publication: First order Büchi automata and their application to verification of LTL specifications