bluuebunny/crossref_metadata_2025_split huggingface dataset:
Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic
Authors: Faggian Claudia , Guerrieri Giulio 
Published: March 2021

AbstractIn each variant of the $$\lambda $$
λ
-calculus, factorization and normalization are two key properties that show how results are computed. Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the $$\lambda $$
λ
-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV.The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.
Focused Proof-search in the Logic of Bunched Implications
Authors: Gheorghiu Alexander , Marin Sonia 
Published: March 2021

AbstractThe logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications.
On the Expressiveness of Büchi Arithmetic
Authors: Haase Christoph , Różycki Jakub 
Published: March 2021

AbstractWe show that the existential fragment of Büchi arithmetic is strictly less expressive than full Büchi arithmetic of any base, and moreover establish that its $$\varSigma _2$$

Σ
2

-fragment is already expressively complete. Furthermore, we show that regular languages of polynomial growth are definable in the existential fragment of Büchi arithmetic.
Parametricity for Primitive Nested Types
Authors: Johann Patricia , Ghiorzi Enrico , Jeffries Daniel 
Published: March 2021

AbstractThis paper considers parametricity and its resulting free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programming perspective and design a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints. Our calculus can express all nested types appearing in the literature, including truly nested types. At the term level, it supports primitive pattern matching, map functions, and fold combinators for nested types. Our main contribution is the construction of a parametric model for our calculus. This is both delicate and challenging: to ensure the existence of semantic fixpoints interpreting nested types, and thus to establish a suitable Identity Extension Lemma for our calculus, our type system must explicitly track functoriality of types, and cocontinuity conditions on the functors interpreting them must be appropriately threaded throughout the model construction. We prove that our model satisfies an appropriate Abstraction Theorem and verifies all standard consequences of parametricity for primitive nested types.
Nondeterministic and co-Nondeterministic Implies Deterministic, for Data Languages
Authors: Klin Bartek , Lasota Sławomir , Toruńczyk Szymon 
Published: March 2021

AbstractWe prove that if a data language and its complement are both recognized by nondeterministic register automata (without guessing), then they are also recognized by deterministic ones.
Certifying Inexpressibility
Authors: Kupferman Orna , Sickert Salomon 
Published: March 2021

AbstractDifferent classes of automata on infinite words have different expressive power. Deciding whether a given language$$L \subseteq \varSigma ^\omega $$L⊆Σωcan be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter in$$\varSigma $$Σ, and Prover responds with an annotation of the current state of the run (for example, in the case of Büchi automata, whether the state is accepting or rejecting, and in the case of parity automata, what the color of the state is). Prover wins if the sequence of annotations she generates is correct: it is an accepting run iff the word generated by Refuter is inL. We show how a winning strategy for Refuter can serve as a simple and easy-to-understand certificate to inexpressibility, and how it induces additional forms of certificates. Our framework handles all classes of deterministic automata, including ones with structural restrictions like weak automata. In addition, it can be used for refutingseparationof two languages by an automaton of the desired class, and for finding automata thatapproximateLand belong to the desired class.
Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP
Authors: Mayr Richard , Schewe Sven , Totzke Patrick , Wojtczak Dominik 
Published: March 2021

AbstractWe study stochastic games with energy-parity objectives, which combine quantitative rewards with a qualitative$$\omega $$ω-regular condition: The maximizer aims to avoid running out of energy while simultaneously satisfying a parity condition. We show that the corresponding almost-sure problem, i.e., checking whether there exists a maximizer strategy that achieves the energy-parity objective with probability 1 when starting at a given energy levelk, is decidable and in$$\mathsf {NP}\cap \mathsf {coNP}$$NP∩coNP. The same holds for checking if such akexists and if a givenkis minimal.
The Structure of Sum-Over-Paths, its Consequences, and Completeness for Clifford
Authors: Vilmart Renaud 
Published: March 2021

AbstractWe show that the formalism of “Sum-Over-Path” (SOP), used for symbolically representing linear maps or quantum operators, together with a proper rewrite system, has the structure of a dagger-compact PROP. Several consequences arise from this observation:– Morphisms of SOP are very close to the diagrams of the graphical calculus called ZH-Calculus, so we give a system of interpretation between the two– A construction, called the discard construction, can be applied to enrich the formalism so that, in particular, it can represent the quantum measurement.We also enrich the rewrite system so as to get the completeness of the Clifford fragments of both the initial formalism and its enriched version.
One-way Resynchronizability of Word Transducers
Authors: Bose Sougata , Krishna S. N. , Muscholl Anca , Puppis Gabriele 
Published: March 2021

AbstractThe origin semantics for transducers was proposed in 2014, and it led to various characterizations and decidability results that are in contrast with the classical semantics. In this paper we add a further decidability result for characterizing transducers that are close to one-way transducers in the origin semantics. We show that it is decidable whether a non-deterministic two-way word transducer can be resynchronized by a bounded, regular resynchronizer into an origin-equivalent one-way transducer. The result is in contrast with the usual semantics, where it is undecidable to know if a non-deterministic two-way transducer is equivalent to some one-way transducer.
Fair Refinement for Asynchronous Session Types
Authors: Bravetti Mario , Lange Julien , Zavattaro Gianluigi 
Published: March 2021

AbstractSession types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is the asynchronous session subtyping, which allows to anticipate message emissions but only under certain conditions. In particular, asynchronous session subtyping rules out candidates subtypes that occur naturally in communication protocols where, e.g., two parties simultaneously send each other a finite but unspecified amount of messages before removing them from their respective buffers. To address this shortcoming, we study fair compliance over asynchronous session types and fair refinement as the relation that preserves it. This allows us to propose a novel variant of session subtyping that leverages the notion of controllability from service contract theory and that is a sound characterisation of fair refinement. In addition, we show that both fair refinement and our novel subtyping are undecidable. We also present a sound algorithm, and its implementation, which deals with examples that feature potentially unbounded buffering.
Running Time Analysis of Broadcast Consensus Protocols
Authors: Czerner Philipp , Jaax Stefan 
Published: March 2021

AbstractBroadcast consensus protocols (BCPs) are a model of computation, in which anonymous, identical, finite-state agents compute by sending/receiving global broadcasts. BCPs are known to compute all number predicates in $$\mathsf {NL}=\mathsf {NSPACE}(\log n)$$

NL
=
NSPACE
(
log
n
)

where n is the number of agents. They can be considered an extension of the well-established model of population protocols. This paper investigates execution time characteristics of BCPs. We show that every predicate computable by population protocols is computable by a BCP with expected $$\mathcal {O}(n \log n)$$

O
(
n
log
n
)

interactions, which is asymptotically optimal. We further show that every log-space, randomized Turing machine can be simulated by a BCP with $$\mathcal {O}(n \log n \cdot T)$$

O
(
n
log
n
·
T
)

interactions in expectation, where T is the expected runtime of the Turing machine. This allows us to characterise polynomial-time BCPs as computing exactly the number predicates in $$\mathsf {ZPL}$$
ZPL
, i.e. predicates decidable by log-space, randomised Turing machine with zero-error in expected polynomial time where the input is encoded as unary.
Directed Reachability for Infinite-State Systems
Authors: Blondin Michael , Haase Christoph , Offtermatt Philip 
Published: March 2021

AbstractNumerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as $$\mathsf {A}^{*}$$

A

∗

and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis.
cake_lpr: Verified Propagation Redundancy Checking in CakeML
Authors: Tan Yong Kiam , Heule Marijn J. H. , Myreen Magnus O. 
Published: March 2021

AbstractModern SAT solvers can emit independently checkable proof certificates to validate their results. The state-of-the-art proof system that allows for compact proof certificates ispropagation redundancy(PR). However, the only existing method to validate proofs in this system with a formally verified tool requires a transformation to a weaker proof system, which can result in a significant blowup in the size of the proof and increased proof validation time. This paper describes the first approach to formally verify PR proofs on a succinct representation; we present (i) a newLinear PR(LPR) proof format, (ii) a tool to efficiently convert PR proofs into LPR format, and (iii) , a verified LPR proof checker developed in CakeML. The LPR format is backwards compatible with the existing LRAT format, but extends the latter with support for the addition of PR clauses. Moreover, is verified using CakeML ’s binary code extraction toolchain, which yields correctness guarantees for its machine code (binary) implementation. This further distinguishes our clausal proof checker from existing ones because unverified extraction and compilation tools are removed from its trusted computing base. We experimentally show that LPR provides efficiency gains over existing proof formats and that the strong correctness guarantees are obtained without significant sacrifice in the performance of the verified executable.
SyReNN: A Tool for Analyzing Deep Neural Networks
Authors: Sotoudeh Matthew , Thakur Aditya V. 
Published: March 2021

AbstractDeep Neural Networks (DNNs) are rapidly gaining popularity in a variety of important domains. Formally, DNNs are complicated vector-valued functions which come in a variety of sizes and applications. Unfortunately, modern DNNs have been shown to be vulnerable to a variety of attacks and buggy behavior. This has motivated recent work in formally analyzing the properties of such DNNs. This paper introduces SyReNN, a tool for understanding and analyzing a DNN by computing its symbolic representation. The key insight is to decompose the DNN into linear functions. Our tool is designed for analyses using low-dimensional subsets of the input space, a unique design point in the space of DNN analysis tools. We describe the tool and the underlying theory, then evaluate its use and performance on three case studies: computing Integrated Gradients, visualizing a DNN’s decision boundaries, and patching a DNN.
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
Authors: Scott Joseph , Niemetz Aina , Preiner Mathias , Nejati Saeed , Ganesh Vijay 
Published: March 2021

AbstractIn this paper, we present MachSMT, an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the SMT-LIB language. It employs machine learning (ML) methods to construct both empirical hardness models (EHMs) and pairwise ranking comparators (PWCs) over state-of-the-art SMT solvers. Given an SMT formula $$\mathcal {I}$$
I
as input, MachSMT leverages these learnt models to output a ranking of solvers based on predicted run time on the formula $$\mathcal {I}$$
I
. We evaluate MachSMT on the solvers, benchmarks, and data obtained from SMT-COMP 2019 and 2020. We observe MachSMT frequently improves on competition winners, winning $$54$$

54

divisions outright and up to a $$198.4$$

198.4

% improvement in PAR-2 score, notably in logics that have broad applications (e.g., BV, LIA, NRA, etc.) in verification, program analysis, and software engineering. The MachSMT tool is designed to be easily tuned and extended to any suitable solver application by users. MachSMT is not a replacement for SMT solvers by any means. Instead, it is a tool that enables users to leverage the collective strength of the diverse set of algorithms implemented as part of these sophisticated solvers.
HLola: a Very Functional Tool for Extensible Stream Runtime Verification
Authors: Gorostiaga Felipe , Sánchez César 
Published: March 2021

AbstractWe present , an extensible Stream Runtime Verification (SRV) tool, that borrows from the functional language Haskell (1) rich types for data in events and verdicts; and (2) functional features for parametrization, libraries, high-order specification transformations, etc.SRV is a formal dynamic analysis technique that generalizes Runtime Verification (RV) algorithms from temporal logics like LTL to stream monitoring, allowing the computation of verdicts richer than Booleans (quantitative values and beyond). The keystone of SRV is the clean separation between temporal dependencies and data computations. However, in spite of this theoretical separation previous engines include hardwired implementations of just a few datatypes, requiring complex changes in the tool chain to incorporate new data types. Additionally, when previous tools implement features like parametrization these are implemented in an ad-hoc way. In contrast, is implemented as a Haskell embedded DSL, borrowing datatypes and functional aspects from Haskell, resulting in an extensible engine (The tool is available open-source athttp://github.com/imdea-software/hlola). We illustrate through several examples, including a UAV monitoring infrastructure with predictive characteristics that has been validated in online runtime verification in real mission planning.
Bridging Arrays and ADTs in Recursive Proofs
Authors: Fedyukovich Grigory , Ernst Gidon 
Published: March 2021

AbstractWe present an approach to synthesize relational invariants to prove equivalences between object-oriented programs. The approach bridges the gap between recursive data types and arrays that serve to represent internal states. Our relational invariants are recursively-defined, and thus are valid for data structures of unbounded size. Based on introducing recursion into the proofs by observing and lifting the constraints from joint methods of the two objects, our approach is fully automatic and can be seen as an algorithm for solving Constrained Horn Clauses (CHC) of a specific sort. It has been implemented on top of the SMT-based CHC solver AdtChc and evaluated on a range of benchmarks.
Momba: JANI Meets Python
Authors: Köhl Maximilian A. , Klauck Michaela , Hermanns Holger 
Published: March 2021

AbstractJANI-model [6] is a model interchange format for networks of interacting automata. It is well-entrenched in the quantitative model checking community and allows modeling a variety of systems involving concurrency, probabilistic and real-time aspects, as well as continuous dynamics. Python is a general purpose programming language preferred by many for its ease of use and vast ecosystem. In this paper, we presentMomba, a flexible Python framework for dealing with formal models centered around the JANI-model format and formalism. Momba strives to deliver an integrated and intuitive experience for experimenting with formal models making them accessible to a broader audience. To this end, it provides a pythonic interface for model construction, validation, and analysis. Here, we demonstrate these capabilities.
Software Verification: 10th Comparative Evaluation (SV-COMP 2021)
Authors: Beyer Dirk 
Published: March 2021

AbstractSV-COMP 2021 is the 10th edition of the Competition on Software Verification (SV-COMP), which is an annual comparative evaluation of fully automatic software verifiers for C and Java programs. The competition provides a snapshot of the current state of the art in the area, and has a strong focus on reproducibility of its results. The competition was based on 15 201 verification tasks for C programs and 473 verification tasks for Java programs. Each verification task consisted of a program and a property (reachability, memory safety, overflows, termination). SV-COMP 2021 had 30 participating verification systems from 27 teams from 11 countries.
A Two-Phase Approach for Conditional Floating-Point Verification
Authors: Lohar Debasmita , Jeangoudoux Clothilde , Sobel Joshua , Darulova Eva , Christakis Maria 
Published: March 2021

AbstractTools that automatically prove the absence or detect the presence of large floating-point roundoff errors or the special values NaN and Infinity greatly help developers to reason about the unintuitive nature of floating-point arithmetic. We show that state-of-the-art tools, however, support or provide non-trivial results only for relatively short programs. We propose a framework for combining different static and dynamic analyses that allows to increase their reach beyond what they can do individually. Furthermore, we show how adaptations of existing dynamic and static techniques effectively trade some soundness guarantees for increased scalability, providing conditional verification of floating-point kernels in realistic programs.
JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution)
Authors: Mues Malte , Howar Falk 
Published: March 2021

AbstractJDartperforms dynamic symbolic execution ofJavaprograms: it executes programs with concrete inputs while recording symbolic constraints on executed program paths. A portfolio of constraint solvers is then used for generating new concrete values from recorded constraints that drive execution along previously unexplored paths. For SV-COMP 2021, we improvedJDartby implementing exploration strategies, bounded analysis, and path-specific constraint solving strategies, as well as by enabling the use of SMT-Lib string theory for encoding of string operations.
Symbiotic 8: Beyond Symbolic Execution
Authors: Chalupa Marek , Jašek Tomáš , Novák Jakub , Řechtáčková Anna , Šoková Veronika , Strejček Jan 
Published: March 2021

AbstractSymbiotic 8 extends the traditional combination of static analyses, instrumentation, program slicing, and symbolic execution with one substantial novelty, namely a technique mixing symbolic execution with k-induction. This technique can prove the correctness of programs with possibly unbounded loops, which cannot be done by classic symbolic execution.Symbiotic 8 delivers also several other improvements. In particular, we have modified our fork of the symbolic executorKleeto support the comparison of symbolic pointers. Further, we have tuned the shape analysis toolPredator(integrated already inSymbiotic 7) to perform better onllvmbitcode. We have also developed a light-weight analysis of relations between variables that can prove the absence of out-of-bound accesses to arrays.
Local Search with a SAT Oracle for Combinatorial Optimization
Authors: Cohen Aviad , Nadel Alexander , Ryvchin Vadim 
Published: March 2021

AbstractNP-hard combinatorial optimization problems are pivotal in science and business. There exists a variety of approaches for solving such problems, but for problems with complex constraints and objective functions, local search algorithms scale the best. Such algorithms usually assume that finding a non-optimal solution with no other requirements is easy. However, what if it is NP-hard? In such case, a SAT solver can be used for finding the initial solution, but how can one continue solving the optimization problem? We offer a generic methodology, called Local Search with SAT Oracle (), to solve such problems. facilitates implementation of advanced local search methods, such as variable neighbourhood search, hill climbing and iterated local search, while using a SAT solver as an oracle. We have successfully applied our approach to solve a critical industrial problem of cell placement and productized our solution at Intel.