Program

Click here for the Schedule.

Click here to return to Workshop Homepage.

Invited Speaker

Author: Jeremy Avigad (Carnegie Mellon University)
Title: The Lean Theorem Prover
Slides: Click here for the slides.
Abstract: Lean is a new interactive theorem prover that is based on dependent type theory. The system is designed to combine interactive theorem proving, computation, and automation within the same logical framework. Dependent type theory provides an expressive language for reasoning about concrete and abstract mathematical structures, and the fact that it has a computational interpretation means that Lean can be used as a programming language as well. With a suitable interface to the system internals, it can also be used as a metaprogramming language, that is, a language with which one can extend the functionality of the system itself. I will survey all these aspects of the system in this talk, and consider ways that Lean can be used as a platform to unify symbolic combination, automated reasoning, and verified proof. In particular, I will describe a Lean-Mathematica connection developed by Robert Y. Lewis, which takes advantage of Lean's metaprogramming capabilities.

---

Full Papers

• Author: Jan Horacek and Martin Kreuzer
  Title: On Conversions from CNF to ANF
  Paper: Click here for the final pdf.
  Slides: Click here for the slides.
  Abstract: In this paper we discuss conversion methods from the conjunctive normal form (CNF) to the algebraic normal form (ANF) of a Boolean function. Whereas the reverse conversion has been studied before, the CNF to ANF conversion has been achieved predominantly via a standard method which tends to produce many polynomials of high degree. Based on a block-building mechanism, we design a new blockwise algorithm for the CNF to ANF conversion which is geared towards producing fewer and lower degree polynomials. In particular, we look for as many linear polynomials as possible in the converted system and check that our algorithm finds them. Experiments show that the ANF produced by our algorithm outperforms the standard conversion in ``real life'' examples originating from cryptographic attacks.
  
  
• Author: Tarik Viehmann, Gereon Kremer and Erika Ábrahám
  Title: Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving
  Paper: Click here for the final pdf.
  Slides: Click here for the slides.
  Abstract: Satisfiability-modulo-theories (SMT) solving is a technique to check the satisfiability of logical formulas. In the context of SMT solving for non-linear real arithmetic, the cylindrical algebraic decomposition (CAD) can be embedded as a theory solver to solve sets (conjunctions) of polynomial constraints. When developing such a CAD theory solver, a design choice is given by the selection of the projection operator used in the CAD method. In this paper we provide some experimental evaluations to analyse how the choice of the projection operator affects the computational efficiency of SMT solving.
  
  
• Author: Martin Brain, James H. Davenport and Alberto Griggio
  Title: Benchmarking Solvers, SAT-style
  Paper: Click here for the final pdf.
  Slides: Click here for the slides.
  Abstract: The SAT community, and hence the SMT community, have substantial experience in bench-marking solvers against each other on large sample sets, and publishing summaries, whereas the computer algebra community tends to time solvers on a small set of problems, and publishing individual times. This paper aims to document the SAT community practice for the benefit of the computer algebra community.

---

Extended Abstracts

• Author: Rui-Juan Jing and Marc Moreno Maza
  Title: Computing the Integer Points of a Polyhedron
  Paper: Click here for the final pdf.
  Slides: Click here for the slides.
  Abstract: Let K be a polyhedron in R^d, given by a system of m linear inequalities, with rational number coefficients bounded over in absolute value by L. We propose an algorithm for computing an irredundant representation of the integer points of K, in terms of “simpler” polyhedra, each of them having at least one integer point. Using the terminology of W. Pugh: for any such polyhedron P, no integer point of its grey shadow extends to an integer point of P. We show that, under mild assumptions, our algorithm runs in exponential time w.r.t. d and in polynomial w.r.t m and L. We report on a software experimentation.
  
  
• Author: Maximilian Jaroschek, Andreas Humenberger and Laura Kovács
  Title: Polynomial Invariant Generation for Multi-Path Loops
  Paper: Click here for the final pdf.
  Slides: Click here for the slides.
  Abstract: Computing loop invariants, that is properties which hold after any number of loop iterations, is a major task in program analysis. In this paper we study nested loops and loops with conditionals. In particular, we generalize a known invariant generating procedure for P-solvable multi-path loops to a wider class of admissible programs, so called extended P-solvable loops.
  
  
• Author: Erika Abraham, Jasper Nalbach and Gereon Kremer
  Title: Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework
  Paper: Click here for the final pdf.
  Slides: Click here for the slides.
  Abstract: Satisfiability-modulo-theories (SMT) solving is a technique to check the satisfiability of logical formulas. In the context of SMT solving, recently a novel technique called the model-constructing satisfiability calculus (MCSAT) was introduced, with a nice embedding of the cylindrical algebraic decomposition method as a theory solving module for non-linear real arithmetic. In this paper we report on our work in progress on the embedding of the virtual substitution method in the MCSAT framework.
  
  
• Author: John Abbott and Anna Maria Bigatti
  Title: New in CoCoA-5.2.0 and CoCoALib-0.99550 for SC-Square
  Paper: Click here for the final pdf.
  Slides: Click here for the slides.
  Abstract: CoCoA-5 is an interactive Computer Algebra System for Computations in Commutative Algebra, particularly Gr\"obner bases. It offers a dedicated, mathematician-friendly programming language, with many built-in functions. Its mathematical core is CoCoALib, an open-source C++ library, designed to facilitate integration with other software. We give an overview of the latest developments of the library and of the system, in particular relating to the project SC-Square.
  
  
• Author: Stephen Forrest
  Title: Integration of SMT-LIB support into Maple
  Paper: Click here for the final pdf.
  Slides: Click here for the slides.
  Abstract: The SC-Square project arose out of the recognition that the Computer Algebra and Satisfiability Checking communities mutually benefit from the sharing of results and techniques. An SMT solver can profit from the inclusion of computer algebra techniques in their theory solvers, while a computer algebra system can profit from dispatching SAT or SMT queries which arise as sub-problems during computation to a dedicated external solver; many existing implementations for both of these may be found. Here we describe on-going work in the second category: specifically, we describe an API in Maple for dispatching computations to, and processing results from, an SMT solver supporting the SMT-LIB format.

---

Presentations Without Publication

• Author: Daniela Ritirc, Armin Biere and Manuel Kauers
  Title: Complexity of circuit ideal membership testing
  Slides: Click here for the slides.
  Abstract: Verifying arithmetic circuits and most prominently multipliers remains an important problem, but in practice still requires substantial manual effort. It was conjectured that verification using SAT solving requires exponential resolution proofs. Recent work tries to overcome this issue by using computer algebra. The most promising approach uses algebraic reasoning over pseudo boolean polynomials. In this talk we revisit and prove soundness and completeness of this approach which allows us to draw some interesting insights in the complexity of the ideal membership problem.
  
  
• Author: Deepak Kapur
  Title: Nonlinear Polynomials, Interpolants and Invariant Generation for System Analysis
  Paper: Click here for the submitted pdf (final version coming soon).
  Slides: Click here for the slides.
  Abstract: Invariant properties at various program locations play a critical role in enhancing confidence in the reliability of software, hardware and hybrid systems. While there has recently been considerable interest in researching heuristics for generating loops invariants, almost all developments have focused on generating invariants typically handled using SMT solvers including propositional formulas, difference and octagonal formulas and linear formulas. While we have been investigating methods based on symbolic computation algorithms including Groebner basis and approximate quantifier elimination for over a decade, the SMT and CAV community have only recently started considering nonlinear polynomial invariants since many programs, especially linear filters, hybrid systems, and other applications, need nonlinear invariants for analysis of their behavior.
  We present an overview of our research with a focus on our most recent work on nonlinear invariant and nonlinear interpolant generation from the perspective of their role in software and hybrid system analysis. Our approach is in sharp contrast to some recent approaches in which nonlinear polynomials are approximated using linear inequalities and symbolic-numeric techniques. We will outline problems and challenges faced by the SMT community for incorporate nonlinear reasoning in their tools as well as issues we encounter in our research.
  
  
• Author: Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm and Xuan Tung Vu
  Title: Subtropical Satisfiability
  Link to Paper: https://arxiv.org/abs/1706.09236.
  Slides: Click here for the slides.
  Abstract: Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of a single very large multivariate polynomial. Our method takes as input conjunctions of strict polynomial inequalities, which represent more than 40\% of the QF\_NRA section of the SMT-LIB library of benchmarks. The method takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. It then uses, in turn, SMT to solve linear problems over the reals to heuristically find suitable points that translate back to satisfying points for the original problem. Systematic experiments on the SMT-LIB demonstrate that our method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques.
  
  
• Author: Martin Bromberger and Christoph Weidenbach
  Title: Computing a Complete Basis for Equalities Implied by a System of LRA Constraints
  Link to Paper: http://ceur-ws.org/Vol-1617/paper2.pdf.
  Link to Extended Paper: https://doi.org/10.1007/s10703-017-0278-7.
  BibTex Entries for above: Click here for BibTex entries for the above papers.
  Slides: Click here for the slides.
  Abstract: We present three new methods that investigate the equalities implied by a system of linear arithmetic constraints. Implied equalities can be used to simplify linear arithmetic constraints and are valuable in the context of Nelson-Oppen style combinations of theories. The first method efficiently checks whether a system of linear arithmetic constraints implies an equality at all. In case the system does, the method also returns a valid equality as an explanation. The second method uses the first method to compute a basis for all implied equalities, i.e., a finite representation of all equalities implied by the linear arithmetic constraints. The third method uses the second method to check efficiently whether a system of linear arithmetic constraints implies a given equality.
  
  
• Author: Curtis Bright, Ilias Kotsireas and Vijay Ganesh
  Title: A SAT+CAS Method for Enumerating Williamson Matrices of Even Order
  Link to Paper: https://sites.google.com/site/uwmathcheck/publications/willeven.pdf.
  Slides: Click here for the slides.
  Abstract: We present for the first time a complete enumeration of Williamson matrices of even order n <= 45. The enumeration method relies on the recently proposed SAT+CAS paradigm of coupling SAT solvers with computer algebra systems, thereby taking advantage of the advances made in both the field of satisfiability checking and the field of symbolic computation. Our results show that Williamson matrices of even order tend to be more abundant than those of odd orders; such matrices exist for every even order in which we performed a search but they do not exist for some odd orders.

---