LOPSTR Conference Programme

Venue: Online via Zoom.

Speaker names are in boldface below.

Monday 7 September 2020, CEST times (UTC+2)

10.30-11:00 BOPL Opening and LOPSTR welcome message

11:00-12:30 Session 1: Rewriting. Chair: Delia Kesner
11:00
Sarah Winkler and Georg Moser
Runtime Complexity Analysis of Logically Constrained Rewriting
11:30
Kentaro Kikuchi and Takahito Aoto
Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables
12:00
Horatiu Cirstea, Pierre Lermusiaux and Pierre-Etienne Moreau
Pattern eliminating transformations
12:30-14:00 BOPL Lunch Break
14:00-15:00 Session 2: Unification. Chair: Temur Kutsia
14:00
Manfred Schmidt-Schauss and Yunus David Kerem Kutz
Nominal Unification with Letrec and Environment-Variables
14:30
Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen
Terminating Non-Disjoint Combined Unification
15:00-15:30 BOPL Coffee Break
15:30-16:30 Session 3: LOPSTR Invited Talk. Chair: Emanuele De Angelis
15:30
Philipp Rümmer
On Constrained Horn Clauses and Program Verification
Abstract: Constrained Horn Clauses (CHC) have over the last decade emerged as a uniform framework for reasoning about different aspects of software safety. CHC form a fragment of first-order logic, modulo various background theories, in which models can be constructed effectively with the help of model checking algorithms. In the talk I will give an overview of CHC, including their use in program verification and the recently established competition CHC-COMP. I will then present some of our work on the construction of CHC solvers that can handle relevant data-types such as integers, bit-vectors, ADTs, and heap.
slides
16:30-17:00 BOPL Tea Break
17:00-18:00 Session 4: Types. Chair: Mário Florido
17:00
Frantisek Farka
slepice: Towards a Verified Implementation of Type Theory in Type Theory
17:30
Jack Hughes and Dominic Orchard
Resourceful Program Synthesis from Graded Linear Types
LOPSTR 2020 Best Paper Award Winner

Tuesday 8 September 2020, CEST times (UTC+2)

11:00-12:30 Session 5: Synthesis, Verification. Chair: Germán Vidal
11:00
Roberto Amadini, Mak Andrlon, Graeme Gange, Peter Schachte, Harald Sondergaard and Peter J. Stuckey
Algorithm Selection for Dynamic Symbolic Execution: a Preliminary Study
11:30
Mario Wenzel and Stefan Brass
Translation of Interactive Datalog Programs for Microcontrollers to Finite State Machines
12:00
Sarat Chandra Varanasi, Neeraj Mittal and Gopal Gupta
Pointer Data Structure Synthesis from Answer Set Programming Specifications
12:30-14:00 BOPL Lunch Break
14:00-15:00 Session 6: Model Checking and Probabilistic Programming. Chair: René Thiemann
14:00
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman and Tobias Winkler.
Generating Functions for Probabilistic Programs
14:30
Soeren Enevoldsen, Mathias Claus Jensen, Kim Guldstrand Larsen, Anders Mariegaard and Jiri Srba
Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs
15:00-15:30 BOPL Coffee Break
15:30-16:30 Session 7: BOPL Invited Talk. Chair: Maurizio Gabbrielli
15:30
José Meseguer
Symbolic Computation in Maude: Some Tapas

Abstract: Maude is a high-performance declarative language based on rewriting logic, supporting declarative concurrent system specification and programming with rewrite theories, and functional programming with equational theories. Besides execution by rewriting and model checking, Maude also supports a wide range of symbolic methods, including: (1) B-unification modulo axioms B of associativity and/or commutativity and/or identity; (2) generalization modulo such axioms B; (3) E,B-variants and (4) (E U B)-unification for E convergent equations modulo B; (5) domain-specific SMT solving through interfaces to CVC4 and Yices; (6) theory-generic SMT solving for initial algebras of theories with the finite variant property (FVP) and OS-compact constructors; and (7) symbolic reachability analysis with topmost transition rules modulo an FVP equational theory. Of these symbolic methods, (3), (4), (5), and (7) are both theory-generic and user-definable, and therefore much more widely applicable than domain-specific algorithms. The talk focuses on these four methods, illustrating them with many examples as "tapas." The main interest of all the above methods, including the chosen four, is that they make it easy to build many formal verification tools in Maude with high degrees of automation, making Maude not just a declarative programming language, but a formal framework for programming and verification. slides

Wednesday 9 September 2020, CEST times (UTC+2)

11:00-12:30 Session 8: Program Analysis and Testing. Chair: María Alpuente
11:00
Ignacio Casso, Jose F. Morales, Pedro Lopez-Garcia and Manuel V. Hermenegildo
Testing Your (Static Analysis) Truths
11:30
Carlos Galindo, Sergio Perez Rubio and Josep Silva
Slicing unconditional jumps with unnecessary control dependencies
12:00
Thom Fruehwirth
Repeated Recursion Unfolding for Super-Linear Speedup
12:30-14:00 BOPL Lunch Break
14:00-15:00 Session 9: Logics. Chair: Mauricio Ayala-Rincón
14:00
Satoshi Matsuoka
A Formal Model for a Linear Time Correctness Condition of Proof Nets of Multiplicative Linear Logic
14:30
Paul Tarau
Synthesis of Modality Definitions and a Theorem Prover for Epistemic Intuitionistic Logic
15:00-15:30 BOPL Coffee Break
15:30-16:30 Session 10: PPDP/LOPSTR Invited Talk. Chair: Maribel Fernández
15:30
Ekaterina Komendantskaya
Continuous Verification of AI: a Declarative Programming Approach
abstract
slides
16:30 Closing