title: 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization

authors:
Muqsit Azeem
Debraj Chakraborty
Sudeep Kanav
Jan Kretínský
MohammadSadegh Mohagheghi
Stefanie Mohr
Maximilian Weininger

abstract: Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such \emph{huge} MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs. The idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.


venue: vmcai

title: LLOR: Automated Repair of OpenMP Programs

authors:
Utpal Bora
Saurabh Joshi
Gautam Muduganti
Ramakrishna Upadrasta


title: ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks

authors:
Gustav S. Bruhns
Martin P. Hansen
Rasmus Hebsgaard
Frederik M. W. Hyldgaard
Jirí Srba


title: Space-Efficient Model-Checking of Higher-Order Recursion Schemes


title: Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study

authors:
Mario Bucev
Samuel Chassot
Simon Felix
Filip Schramka
Viktor Kuncak


title: Constructing Trustworthy Smart Contracts

authors:
Devora Chait-Roth
Kedar S. Namjoshi


title: Two-Way Collaboration Between Flow and Proof in SPARK

authors:
Claire Dross
Joffrey Huguet
Johannes Kanig


title: Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction

authors:
Paul Eichler
Swen Jacobs
Chana Weil-Kennedy

abstract: We introduce a new framework for verifying systems with a parametric number of concurrently running processes. The systems we consider are well-structured with respect to a specific well-quasi order. This allows us to decide a wide range of verification problems, including control-state reachability, coverability, and target, in a fixed finite abstraction of the infinite state-space, called a 01-counter system. We show that several systems from the parameterized verification literature fall into this class, including reconfigurable broadcast networks (or systems with lossy broadcast), disjunctive systems, synchronizations and systems with a fixed number of shared finite-domain variables. Our framework provides a simple and unified explanation for the properties of these systems, which have so far been investigated separately. Additionally, it extends and improves on a range of the existing results, and gives rise to other systems with similar properties.


title: Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts

authors:
Julian Erhard
Manuel Bentele
Matthias Heizmann
Dominik Klumpp
Simmo Saan
Frank Schüssele
Michael Schwarz
Helmut Seidl
Sarah Tilscher
Vesal Vojdani


title: A Real-Blasting Extension of cvc5 for Reasoning About Floating-Point Arithmetic


title: Affine Disjunctive Invariant Generation with Farkas' Lemma

authors:
Jingyu Ke
Hongfei Fu
Hongming Liu
Zhouyue Sun
Liqian Chen
Guoqiang Li


title: Synthesis of Controllers for Continuous Blackbox Systems

authors:
Benedikt Maderbacher
Felix Windisch
Alberto Larrauri
Roderick Bloem


title: Abstract Local Completeness - A Local Form of Abstract Non-interference


title: An Abstract Domain for Heap Commutativity

authors:
Jared Pincus
Eric Koskinen


title: Property-Agnostic Base Case Extension for Scalable Verification of Distributed Systems

authors:
Kyle Storey
Eric Mercer


title: Automatic Inference of Relational Object Invariants

authors:
Yusen Su
Jorge A. Navas
Arie Gurfinkel
Isabel Garcia-Contreras


title: Automated Flaw Detection for Industrial Robot RESTful Service

authors:
Yuncheng Wang
Puzhuo Liu
Yaowen Zheng
Dongliang Fang
Shuaizong Si
Zhiwen Pan
Weidong Zhang
Limin Sun


title: Discovering Likely Invariants for Distributed Systems Through Runtime Monitoring and Learning

authors:
Yuan Xia
Deepayan Sur
Aabha Shailesh Pingle
Jyotirmoy V. Deshmukh
Mukund Raghothaman
Srivatsan Ravi


title: Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training

authors:
Junfeng Yang
Min Zhang
Xin Chen
Qin Li


title: Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications

authors:
Ruoxi Zhang
Richard J. Trefler
Kedar S. Namjoshi


title: Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver

authors:
Bruno Andreotti
Haniel Barbosa


title: Reachability in Multi-agent Transfer Systems

authors:
Nathalie Bertrand
Loïc Hélouët
Engel Lefaucheux
Luca Paparazzo


title: Efficiently Verifying Quantum Programs with Few T Gates

authors:
Youngchan Cho
Robert Rand


title: Atomic Gliders and Cellular Automata as Language Generators

authors:
Dana Fisman
Noa Izsak


title: A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamic Systems

authors:
Rui Guo
Yang Li
Xiuqing Cao
Wang Lin


title: Proof Minimization in Neural Network Verification

authors:
Omri Isac
Idan Refaeli
Haoze Wu
Clark W. Barrett
Guy Katz


title: Finding Photonics Circuits via δ-Weakening SMT

authors:
Marco Lewis
Benoît Valiron

abstract: For quantum computers based on photonics, one main problem is the synthesis of a photonic circuit that emulates quantum computing gates. The problem requires using photonic components to build a circuit that act like a quantum computing gate with some probability of success. This involves not only finding a circuit that can correctly act like a quantum gate, but also optimizing the probability of success. Whilst many approaches have been given in the past and applied to specific gates, they often lack ease of reusability. We present a tool that uses dReal, a {\delta}-weakening SMT solver, to find such photonic circuits, optimize the likelihood of occurring, and provide some guarantee that the result is optimal. We demonstrate the usage of our tool by recreating known results in the literature, extending upon them, and presenting new results for Givens rotation gates.


title: Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification

authors:
Andreas Lindner
Karl Palmskog
Scott Constable
Mads Dam
Roberto Guanciale
Hamed Nemati

abstract: Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when certifying properties of binary (machine) code in trustworthy systems, e.g., cryptographic routines. We present a theory of forward symbolic execution for unstructured programs suitable for use in theorem provers that enables automated verification of both functional and non-functional program properties. The theory's foundation is a set of inference rules where each member corresponds to an operation in a symbolic execution engine. The rules are designed to give control over the tradeoff between the preservation of precision and introduction of overapproximation. We instantiate our theory for BIR, a previously proposed intermediate language for binary analysis. We demonstrate how symbolic executors can be constructed for BIR with common optimizations such as pruning of infeasible symbolic states. We implemented our theory in the HOL4 theorem prover using the HolBA binary analysis library, obtaining machine-checked proofs of soundness of symbolic execution for BIR. We practically evaluated two applications of our theory: verification of functional properties of RISC-V binaries and verification of execution time bounds of programs running on the ARM Cortex-M0 processor. The evaluation shows that such verification can be automated with moderate overhead on medium-sized programs.


title: SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation

authors:
Junjie Meng
Jie An
Yong Li
Andrea Turrini
Miaomiao Zhang


title: Try-Mopsa: Relational Static Analysis in Your Pocket


title: Input-Based Three-Valued Abstraction Refinement

authors:
Jan Onderka
Stefan Ratschan

abstract: Unlike Counterexample-Guided Abstraction Refinement (CEGAR), Three-Valued Abstraction Refinement (TVAR) is able to verify all properties of the mu-calculus. We present a novel algorithmic framework for TVAR that employs a simulator-like approach to build and refine the abstract state space with input-based splitting. This leads to a state space formalism that is much simpler than in previous TVAR frameworks, which use modal transitions. We implemented the framework in our open-source tool machine-check and verified properties of machine-code systems for the AVR architecture, showing the ability to verify systems and mu-calculus properties not verifiable by naive model checking or CEGAR, respectively. This is the first practical use of TVAR for machine-code verification.


title: Efficient Discovery of Actual Causality in Stochastic Systems

authors:
Arshia Rafieioskouei
Kenneth Rogale
Borzoo Bonakdarpour

abstract: Identifying the actual cause of events in engineered systems is a fundamental challenge in system analysis. Finding such causes becomes more challenging in the presence of noise and stochastic behavior in real-world systems. In this paper, we adopt the notion of probabilistic actual causality by Fenton-Glynn, which is a probabilistic extension of Halpern and Pearl's actual causality, and propose a novel method to formally reason about causal effect of events in stochastic systems. We (1) formulate the discovery of probabilistic actual causes in computing systems as an SMT problem, and (2) address the scalability challenges by introducing an abstraction-refinement technique that improves efficiency by up to 95%. We demonstrate the effectiveness of our approach through three case studies, identifying probabilistic actual causes of safety violations in (1) the Mountain Car problem, (2) the Lunar Lander benchmark, and (3) MPC controller for an F-16 autopilot simulator.


title: Termination Resilience Static Analysis

authors:
Naïm Moussaoui Remil
Caterina Urban


title: Verification of Generic VHDL Designs and Their Translation to Rocq

authors:
Ocan Sankur
Benoît Boyer
Florian Faissole


title: Data Race Detection by Digest-Driven Abstract Interpretation

authors:
Michael Schwarz
Julian Erhard


title: Multi-variable Quantification of BDDs in External Memory using Nested Sweeping

authors:
Steffan Christ Sølvsten
Jaco van de Pol


title: A Formal Executable Semantics of PROMELA

authors:
Byoungho Son
Kyungmin Bae


title: Probabilistic Verification for Modular Network-on-Chip Systems

authors:
Nick Waddoups
Jonah Boe
Arnd Hartmanns
Prabal Basu
Sanghamitra Roy
Koushik Chakraborty
Zhen Zhang