相关论文: Modeling and Verification of Infinite Systems with…

A circular program contains a data structure whose definition is self-referential or recursive. The use of such a definition allows efficient functional programs to be written and can avoid repeated evaluations and the creation of…

We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are first-order definable in a fixed countably-infinite structure. We show that the reachability analysis can be addressed…

We present a compositional framework for certifying resource bounds in typed programs. Terms are typed with synthesized bounds drawn from an abstract resource lattice, enabling uniform treatment of time, memory, gas, and domain-specific…

We introduce a set of eight universal Rules of Inference by which computer programs with known properties (axioms) are transformed into new programs with known properties (theorems). Axioms are presented to formalize a segment of Number…

We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines that communicate by reading from and writing to a shared memory. Beyond the…

We consider the problem of automatically verifying programs which manipulate arbitrary data structures. Our specification language is expressive, contains a notion of \emph{separation}, and thus enables a precise specification of…

We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis,…

Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive procedures and…

We study the problem of automated hypersafety verification of infinite-state recursive programs. We propose an infinite class of product programs, specifically designed with recursion in mind, that reduce the hypersafety verification of a…

We study termination of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions. Reasoning about the termination probability of programs with continuous distributions…

We present a logical framework for the verification of relational properties in imperative programs. Our work is motivated by relational properties which come from security applications and often require reasoning about formulas with…

Ong has shown that the modal mu-calculus model checking problem (equivalently, the alternating parity tree automaton (APT) acceptance problem) of possibly-infinite ranked trees generated by order-n recursion schemes is n-EXPTIME complete.…

Formal verification using the model checking paradigm has to deal with two aspects: The system models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of…

We introduce the first cut-free nested sequent systems for first-order modal logics that admit increasing, decreasing, constant, and empty domains along with so-called general path conditions and seriality. We obtain such systems by means…

We study a type of reverse (procurement) auction problems in the presence of budget constraints. The general algorithmic problem is to purchase a set of resources, which come at a cost, so as not to exceed a given budget and at the same…

In many instances in first order logic or computable algebra, classical theorems show that many problems are undecidable for general structures, but become decidable if some rigidity is imposed on the structure. For example, the set of…

Although many investigators affirm a desire to build reasoning systems that behave consistently with the axiomatic basis defined by probability theory and utility theory, limited resources for engineering and computation can make a complete…

When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into…

Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in theory T. If a sound and complete inference system for…

This paper studies the logical properties of a very general class of infinite ranked trees, namely those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal mu-calculus, three main…