|
10:30-
12:30
|
TACAS:
Constraint Solving
Room: HS1, online: link
Chair: Andreia Mordido
- Randal Bryant, Armin Biere and Marijn Heule. Clausal Proofs for Pseudo-Boolean Reasoning
- Joseph Reeves, Marijn Heule and Randal Bryant. Moving Definition Variables in Quantified Boolean Formulas
- Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K Murali and Christoph Weidenbach. A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
- Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar. cvc5: A Versatile and Industrial-Strength SMT Solver [nominated for SCP best tool paper]
|
TACAS:
Monitoring and Analysis
Room: HS2, online: link
Chair: Ezio Bartocci
- Pu Yi, Hao Wang, Tao Xie, Darko Marinov and Wing Lam. A Theoretical Analysis of Random Regression Test Prioritization
- Sheila Zingg, Srdjan Krstic, Martin Raszyk, Joshua Schneider and Dmitriy Traytel. Verified First-Order Monitoring with Recursive Rules
- Ilia Zlatkin and Grigory Fedyukovich. Maximizing Branch Coverage with Constrained Horn Clauses
- Marco Bozzano, Alessandro Cimatti, Alberto Griggio and Martin Jonáš. Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation
|
FoSSaCS:
Categorical Models
Room: Interims HS1, online: link
Chair: Jurriaan Rot
- Anne Broadbent and Martti Karvonen. Categorical composable cryptography
- Davide Castelnovo, Fabio Gadducci and Marino Miculan. A new criterion for M,N-adhesivity, with an application to hierarchical graphs
- Dylan McDermott, Exequiel Rivas and Tarmo Uustalu. Sweedler Theory of Monads
- Guillaume Boisseau and Robin Piedeleu. Graphical Piecewise-Linear Algebra
|
ESOP:
Verified Systems
Room: HS3, online: link
Chair: Peter Müller
- Jorge Sousa Pinto, Cláudio Belo Lourenço. Why3-do: The Way of Harmonious Distributed System Proofs [nominated for SCP best tool paper]
- Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell. Relaxed virtual memory in Armv8-A [nominated for EASST best paper]
- Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell. Verified Security for the Morello Capability-enhanced Prototype Arm Architecture
- David Monniaux, Sylvain Boulmé. The Trusted Computing Base of the CompCert Verified Compiler
|
|
14:00-
16:00
|
TACAS: Model checking and verification
Room: HS1, online: link
Chair: Alexandra Silva
- Nicolas Amat, Silvano Dal Zilio and Thomas Hujsa. Property Directed Reachability for Generalized Petri Nets
- Martin Blicha, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina. Transition Power Abstractions for Deep Counterexample Detection
- Marco Bozzano, Alessandro Cimatti, Stefano Tonetta and Viktória Vozárová. Searching for Ribbon-Shaped Paths in Fair Transition Systems
- Dirk Beyer and Sudeep Kanav. CoVeriTeam: On-Demand Composition of Cooperative Verification Systems
|
|
FoSSaCS:
Types
Room: Interims HS1, online: link
Chair: Robert Atkey
- Simon Gay, Diogo Poças and Vasco Vasconcelos. The Different Shades of Infinite Session Types
- Emmanuel Hainry, Bruce Kapron, Jean-Yves Marion and Romain Péchoux. Complete and tractable machine-independent characterizations of second-order polytime [nominated for EAPLS and EATCS best paper]
- José Espírito Santo, Delia Kesner and Loïc Peyrot. A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications
- André Hirschowitz, Tom Hirschowitz, Ambroise Lafont and Marco Maggesi. Variable binding and substitution for (nameless) dummies
|
ESOP:
Concurrency I
Room: HS3, online: link
Chair: Rupak Majumdar
- Eleni Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson. View-Based Owicki–Gries Reasoning for Persistent x86-TSO
- Artem Khyzha, Ori Lahav. Abstraction for Crash-Resilient Objects
- Varsha P Suresh, Deepak D'Souza, Rekha Pai, Meenakshi D'Souza, Sujit Kumar Chakrabarti. Static Race Detection for Periodic Programs
- Parosh Aziz Abdulla and Mohamed Faouzi Atig, Raj Aryan Agarwal, Adwait Godbole, Krishna S. Probabilistic Total Store Ordering
|