Argument Reduction of Constrained Horn Clauses Using Equality Constraints
Abstract elided by the publisher.
26,098 papers · page 155 of 1,305
Transport via Partial Galois Connections and Equivalences
Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees. Similarly, subtypes and quotients are commonly …
A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists
Abstract elided by the publisher.
Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection
Abstract elided by the publisher.
Types and Semantics for Extensible Data Types
Abstract elided by the publisher.
Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq
Abstract elided by the publisher.
TorchProbe: Fuzzing Dynamic Deep Learning Compilers
Abstract elided by the publisher.
What Types Are Needed for Typing Dynamic Objects? A Python-Based Empirical Study
Abstract elided by the publisher.
Compilation Semantics for a Programming Language with Versions
Abstract Programming with versions is a paradigm that allows a program to use multiple versions of a module so that the programmer can selectively use functions from both older and newer versions of a single module. Previous work formalized $$\lambda _{\textrm{VL}}$$ λ VL , a cor…
Proofs as Terms, Terms as Graphs
. Starting from an encoding of untyped λ -terms with sharing, defined using synthetic inference rules based on a focused proof system for Gentzen’s LJ , we introduce the positive λ -calculus, a call-by-value calculus with explicit substitutions. This calculus is closely related t…
Towards a Framework for Developing Verified Assemblers for the ELF Format
Abstract Most of the existing work on verified compilation leaves unverified the translation of assembly programs into binary code in object file formats (e.g., the Executable and Linkable Format or ELF). The challenges of developing verified assemblers come from the intrinsic co…
Overcoming Memory Weakness with Unified Fairness - Systematic Verification of Liveness in Weak Memory Models
Abstract We consider the verification of liveness properties for concurrent programs running on weak memory models. To that end, we identify notions of fairness that preclude demonic non-determinism, are motivated by practical observations, and are amenable to algorithmic techniq…
Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis
Abstract Given a specification as a Boolean relation between inputs and outputs, Boolean functional synthesis generates a function, called a Skolem function, for each output in terms of the inputs such that the specification is satisfied. In general, there may be many possibiliti…
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
Abstract Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (…
A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation
Abstract In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with t…
Formally Verified EVM Block-Optimizations
Abstract The efficiency and the security of smart contracts are their two fundamental properties, but might come at odds: the use of optimizers to enhance efficiency may introduce bugs and compromise security. Our focus is on (Ethereum Virtual Machine) block-optimizations , which…
Policy Synthesis and Reinforcement Learning for Discounted LTL
Abstract The difficulty of manually specifying reward functions has led to an interest in using linear temporal logic (LTL) to express objectives for reinforcement learning (RL). However, LTL has the downside that it is sensitive to small perturbations in the transition probabili…
Automatic Program Instrumentation for Automatic Verification
Abstract In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verificat…
Verifying Generalization in Deep Learning
Abstract Deep neural networks (DNNs) are the workhorses of deep learning, which constitutes the state of the art in numerous application domains. However, DNN-based decision rules are notoriously prone to poorgeneralization, i.e., may prove inadequate on inputs not encountered du…
Synthesizing Permissive Winning Strategy Templates for Parity Games
Abstract We present a novel method to compute permissive winning strategies in two-player games over finite graphs with $$ \omega $$ ω -regular winning conditions. Given a game graph G and a parity winning condition $$\varPhi $$ Φ , we compute a winning strategy template $$\varPs…