On Complete Reasoning about Axiomatic Specifications
Graph Chatbot
Chat with Graph Search
Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.
DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.
We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term a ...
We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPL ...
Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting the c ...
In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexampl ...
We describe a parameterized decision procedure that extends the decision procedure for functional recursive algebraic data types (trees) with the ability to specify and reason about abstractions of data structures. The abstract values are specified using r ...
Motivated by applications in software verification, we explore automated reasoning about the non-disjoint combination of theories of infinitely many finite structures, where the theories share set variables and set operations. We prove a combination theore ...
We present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. Specifically, we present the use of the Jahob verification system to verify form ...
Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these applications. Multisets arise in these applications for analogous reasons a ...
We prove a general subconvex bound in the level aspect for Rankin–Selberg L-functions associated with two primitive holomorphic or Maass cusp forms over Q. We use this bound to establish the equidistribution of incomplete Galois orbits of Heegner points on ...
The execution of formal specifications is important for verification, validation and animation purposes. This thesis describes transformation of CO-OPN specifications in executable code. The original goal of this transformation was validation by prototypin ...
