previous day
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 9: Scaling Formal Software Verification (Invited Presentation.)

Invited Presentation

Speaker: Gerwin Klein

Scaling Formal Software Verification
SPEAKER: Gerwin Klein
10:00-10:30Coffee Break
10:30-12:15 Session 10: Reasoning in theories
Sharing HOL4 and HOL Light proof knowledge
SPEAKER: unknown

ABSTRACT. New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers or libraries. In this paper we propose and evaluate a number of methods, which strengthen proof automation by learning from proof libraries of different provers. Certain conjectures can be proved directly from the dependencies induced by similar proofs in the other library. Even if exact correspondences are not found, learning-reasoning systems can make use of the association between proved theorems and their characteristics to predict the relevant premises. Such external help can be further combined with internal advice. We evaluate the proposed knowledge-sharing methods by reproving the HOL Light and HOL4 standard libraries. The learning-reasoning system HOL(y)Hammer, whose single best strategy could automatically find proofs for 30\% of the HOL Light problems, can prove 40\% with the knowledge from HOL4.

Abstract Domains and Solvers for Sets Reasoning
SPEAKER: unknown

ABSTRACT. When constructing complex program analyses, it is often useful to reason about not just individual values, but collections of values. Symbolic set abstractions provide such a building block that can be used to construct partitions of elements, relate partitions to other partitions, and determine the provenance of multiple values, all without knowing any concrete values. To address the simultaneous challenges of scalability and precision, we formalize and implement an interface for symbolic set abstractions and construct multiple abstractions relying on both specialized data structures and off-the-shelf theorem provers. Additionally, we develop techniques for lifting existing domains to improve performance and precision. We evaluate these new domains on real-world data structure analysis problems.

Fine grained SMT proofs for the theory of fixed-width bit-vectors
SPEAKER: unknown

ABSTRACT. Many high-level verification tools rely on SMT solvers to efficiently discharge complex verification conditions. Some applications require more than just a yes/no answer from the solver. For satisfiable problems, a satisfying model is a natural artefact. In the unsatisfiable case, an externally checkable proof can serve as a certificate of correctness and can be mined to gain additional insight into the problem.

In this paper we present a method of encoding and checking SMT-generated proofs for the theory of fixed-width bit-vectors. Proof generation and checking for the bit-vector theory poses additional challenges compared to other theories: reducing the problem to propositional logic can result in large resolution proofs as well as requiring a proof that the reduction itself is correct. We describe a fine-grained proof system formalized in the LFSC framework that addresses some of these challenges by the use of computational side-conditions. We instrument the CVC4 SMT solver to automatically generate such proofs and evaluate the performance impact of proof generation.

Playing with Quantified Satisfaction
SPEAKER: unknown

ABSTRACT. We develop an algorithm for satisfiability of quantified formulas. The algorithm is based on recent progress in solving Quantified Boolean Formulas, but it generalizes beyond propositional logic to theories, such as linear arithmetic over integers (Presburger arithmetic), linear arithmetic over reals, algebraic data-types and arrays. Compared with previous algorithms for satisfiability of quantified arithmetical formulas our new implementation outperforms previous implementations in Z3 by a significant margin.

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
SPEAKER: unknown

ABSTRACT. We introduce an encoding of the set theory of the B method using polymorphic types and deduction modulo, which is used for the automated verification of proof obligations in the framework of the BWare project. Deduction modulo is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We also present the associated automated theorem prover Zenon Modulo, an extension of Zenon to polymorphic types and deduction modulo, along with its backend to the Dedukti universal proof checker, which also relies on types and deduction modulo, and which allows us to verify the proofs produced by Zenon Modulo. Finally, we assess our approach over the proof obligation benchmark of BWare.

12:00-14:00Lunch Break
14:00-15:30 Session 11: Logic programming and applications
Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
SPEAKER: unknown

ABSTRACT. In this paper, we investigate the use of high-level action languages for representing and reasoning about ethical responsibility in goal specification domains. First, we present a simplified Event Calculus formulated as a logic program under the stable model semantics in order to represent situations within Answer Set Programming. Second, we introduce a model of causality that allows us to use an answer set solver to perform reasoning over the agent’s ethical responsibility. We then extend and test this framework against the Trolley Problem and the Doctrine of Double Effect. The overarching aim of the paper is to propose a general and adaptable formal language that may be employed over a variety of ethical scenarios in which the agent’s responsibility must be examined and their choices determined. Our fundamental motivation rests in the will to displace the burden of moral reasoning from the programmer to the program itself, moving away from current computational ethics that too easily embed moral reasoning withing the computational engines, thereby feeding atomic answers that fail to truly represent the underlying dynamics at play.

Modular Multiset Rewriting
SPEAKER: unknown

ABSTRACT. Rule-based languages are being used for ever more ambitious applications. As program size grows however, so does the overhead of team-based development, reusing components, and just keeping a large flat collection of rules from interfering. In this paper, we propose a module system for a small logically-motivated rule-based language. The resulting modules are nothing more than rewrite rules of a specific form, which are themselves just logic formulas. Yet, they provide some of the same features found in advanced module systems such as that of Standard ML, in particular name space separation, support for abstract data types, and parametrization (functors in ML). Our modules also offer essential features for concurrent programming such as facilities for sharing private names. This approach is directly applicable to other rule-based languages, including most forward-chaining logic programming languages and many process algebras.

A Fast Interpreter for λProlog
SPEAKER: unknown

ABSTRACT. We present a new interpreter for λProlog that runs consistently faster than the bytecode compiled by Teyjus, that is believed to be the best available implementation for λProlog. The key insight is the identification of a fragment of the language, which we call Reduction-Free Fragment, that occurs quite naturally in λProlog programs and that admits constant time reduction and unification rules. The implementation exploits De Bruijn levels and no explicit substitutions, whereas Teyjus is based on De Bruijn indexes and explicit substitutions (the suspension calculus).

On Conflicts and Strategies in QBF
SPEAKER: unknown

ABSTRACT. QBF solving techniques can be divided into the DPLL-based and expansion-based. In this paper we look at how these two techniques can be combined while using strategy extraction as a means of interaction between the two. Once propagation derives a conflict for one of the players, we analyse the proof of such and devise a strategy for the opponent. Subsequently, this strategy is used to constrain the losing player. The implemented prototype shows feasibility of the approach. A number of avenues for future research can be envisioned. Can strategies be employed in a different fashion? Can better strategy be constructed? Do the presented techniques generalize beyond QBF?

15:30-16:00Coffee Break
16:00-18:00 Session 12: Non-classical logics and reasoning
A Contextual Logical Framework
SPEAKER: unknown

ABSTRACT. A new logical framework with explicit linear contexts and names is presented, with the purpose of enabling direct and flexible manipulation of contexts, both for representing systems and meta-properties. The framework is a conservative extension of the logical framework LF, and builds on linear logic and contextual modal type theory. We prove that the framework admits canonical forms, and that it possesses all desirable meta-theoretic properties, in particular hereditary substitutions.

As proof of concept, we give an encoding of the one-sided sequent calculus for classical linear logic and the corresponding cut-admissibility proof, as well as an encoding of parallel reduction of lambda terms with the corresponding value-soundness proof.

Focused labeled proof systems for modal logic
SPEAKER: unknown

ABSTRACT. Focused proofs are sequent calculus proofs that group inference rules into alternating negative and positive phases. These phases can then be used to define macro-level inference rules from Gentzen's original and tiny introduction and structural rules. We show here that the inference rules of labeled proof systems for modal logics can similarly be described as pairs of such negative and positive phases within the LKF focused proof system (which contains no modal connectives). In particular, we consider the system G3K of Negri for the modal logic K and define a translation from labeled modal formulas into first-order polarized formulas and show a strict correspondence between derivations in the two systems, i.e., each rule application in G3K corresponds to a bipole - a pair of a positive and a negative phases - in LKF. Since geometric axioms (when properly polarized) induce bipoles, this strong correspondence holds for all modal logics whose Kripke frames are characterized by geometric properties. We extend these results to present a focused labeled proof system for this same class of modal logics and show its soundness and completeness. This resulting proof system allows one to define a rich set of normal forms of modal logic proofs.

A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic
SPEAKER: unknown

ABSTRACT. Intuitionistic Public Announcement Logic (IntPAL) proposed by Ma et al. (2014) aims for a formal expression of change of knowledge in a constructive manner. IntPAL is a combination of Public Announcement Logic (PAL) by Plaza (1989) and the intuitionistic modal logic IK by Fischer Servi (1984) and Simpson (1994). We also refer to IK for the basis of this paper. Meanwhile, Nomura et al. (2015) provided a cut-free labelled sequent calculus based on the study of Maffezioli et al. (2010). In this paper, we introduce a labelled sequent calculus for IntPAL (we call it GIntPAL) as both an intuitionistic variant of GPAL and a public announcement extension of Simpson's labelled calculus, and show that all theorems of the Hilbert axiomatization of IntPAL are also provable in GIntPAL with the cut rule. Then we prove the admissibility of the cut rule in GIntPAL and also its soundness for birelational Kripke semantics. Finally, we derive the semantic completeness of GIntPAL as a corollary of these theorems.

Skolemization for Substructural Logics

ABSTRACT. The usual Skolemization procedure, which removes strong quantifiers by introducing new function symbols, is in general unsound for first-order substructural logics defined based on classes of complete residuated lattices. However, it is shown here (following similar ideas of Baaz and Iemhoff for first-order intermediate logics) that first-order substructural logics with a semantics satisfying certain witnessing conditions admit a "parallel" Skolemization procedure where a strong quantifier is removed by introducing a finite disjunction or conjunction (as appropriate) of formulas with multiple new function symbols. These logics typically lack equivalent prenex forms. Also, semantic consequence does not in general reduce to satisfiability. The Skolemization theorems presented here therefore take various forms, applying to the left or right of the consequence relation, and to all formulas or only prenex formulas.

Automated Theorem Proving by Translation to Description Logic
SPEAKER: unknown

ABSTRACT. Many Automated Theorem Proving (ATP) systems for different logics, and translators for translating different logics from one to another, have been developed and are now available. Some logics are more expressive than others, and it is easier to express problems in those logics. However, their ATP systems are relatively newer, and need more development and testing in order to solve more problems in a reasonable time. To benefit from the available tools to solve more problems in more expressive logics, different ATP systems and translators can be combined. Problems in logics more expressive than CNF can be translated directly to CNF, or indirectly by translation via intermediate logics. Description Logic (DL) sits between CNF and propositional logic. Saffron a CNF to DL translator, has been developed, which fills the gap between CNF and DL. ATP by translation to DL is now an alternative way of solving problems expressed in logics more expressive than DL, by combining necessary translators from those logics to CNF, Saffron, and a DL ATP system.