Temporal stream logic (TSL) extends LTL with updates and predicates over arbitrary
function terms. This allows for specifying dataintensive systems for which LTL is not …

In software development, formal program specifications play a crucial role in various stages.
However, manually crafting formal program specifications is rather difficult, making the job …

We identify a decidable synthesis problem for a class of programs of unbounded size with
conditionals and iteration that work over infinite data domains. The programs in our class …

First-order logic, and quantifiers in particular, are widely used in deductive verification of
programs and systems. Quantifiers are essential for describing systems with unbounded …

This paper lays a practical foundation for using abstract interpretation with an abstract
domain that consists of sets of quantified first-order logic formulas. This abstract domain …

Message-passing programs involve several processes with channel-based communications
to deal with tasks concurrently. The complex computations and communications between …

Verifying programs that manipulate tree data structures often requires complex, ad-hoc
proofs that are hard to generalize and automate. This paper introduces an automatic …

The verification of uninterpreted programs is undecidable in general. This paper proposes to
employ counterexample-guided abstraction refinement (CEGAR) framework for verifying …

The classicaldecision problem'asks whether a given formula of first-order logic is satisfiable.
In this work we consider an extension of this problem to regular first-order theories, ie …

Given a set of uninterpreted programs to be verified, the trace abstraction-based verification
method can be used to solve them once at a time. The verification of different programs is …