Related papers: Verified Purely Functional Catenable Real-Time Deq…
We present an efficient and practical lock-free implementation of a concurrent deque that is disjoint-parallel accessible and uses atomic primitives which are available in modern computer systems. Previously known lock-free algorithms of…
We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $\lambda$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to…
While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this paper we present and study the logic rLTL which provides a means to formally reason about both correctness and…
We present our work on the collaborative use of dynamic and static analysis tools for the verification of software written in the OCaml language. We build upon Gospel, a specification language for OCaml that can be used both in dynamic and…
We present a sequent calculus for abstract focussing, equipped with proof-terms: in the tradition of Zeilberger's work, logical connectives and their introduction rules are left as a parameter of the system, which collapses the synchronous…
A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool-chain. An example is the…
We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic…
Virtual integration techniques focus on building architectural models of systems that can be analyzed early in the design cycle to try to lower cost, reduce risk, and improve quality of complex embedded systems. Given appropriate…
We study the enumeration of answers to ontology-mediated queries (OMQs) where the ontology is a set of guarded TGDs or formulated in the description logic ELI and the query is a conjunctive query (CQ). In addition to the traditional notion…
We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The resulting objects we call continuous machines. We prove that…
In this work, we investigate some connections between exact differential equations and harmonic functions and in particular, we obtain necessary and sufficient conditions for which exact equations admit harmonic solutions. As an…
If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a deliberate mechanized formalization gap we can shrink and…
Canonical functions are a powerful concept with numerous applications in the study of groups, monoids, and clones on countable structures with Ramsey-type properties. In this short note, we present a proof of the existence of canonical…
In purely functional programming languages imperative features, more generally computational effects are prohibited. However, non-functional lan- guages do involve effects. The theory of decorated logic provides a rigorous for- malism (with…
The free-variable tableau method has been widely used in order to automate proofs in multiple kinds of logics. Many automated theorem provers rely on this approach, either because it is the only available method-e.g., in certain modal…
We study $Q$-tableaux and axiom systems that they engender, producing a new proof that the Implicational Propositional Calculus is complete.
We show how to extract a monotonic learning algorithm from a classical proof of a geometric statement by interpreting the proof by means of interactive realizability, a realizability sematics for classical logic. The statement is about the…
In this report, we present the preliminary work developed for our research project for the APDC (\'Area Pr\'atica de Desenvolvimento Curricular) course. The main goal of this project is to develop a framework, on top of the Why3 tool, for…
This report documents the process of implementing vector clocks in the Coq proof assistant for extraction and use in the distributed Dynamo-inspired data store, Riak. In this report, we focus on the technical challenges of using Core Erlang…
We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms…