Latest in cs.lo

total 10921took 0.12s
Time-Stamped Claim LogicJul 15 2019The main objective of this paper is to define a logic for reasoning about distributed time-stamped claims. Such a logic is interesting for theoretical reasons, i.e., as a logic per se, but also because it has a number of practical applications, in particular ... More
Solving Mean-Payoff Games via Quasi DominionsJul 14 2019We propose a novel algorithm for the solution of mean-payoff games that merges together two seemingly unrelated concepts introduced in the context of parity games, small progress measures and quasi dominions. We show that the integration of the two notions ... More
Sharing Equality is LinearJul 13 2019The $\lambda$-calculus is a handy formalism to specify the evaluation of higher-order programs. It is not very handy, however, when one interprets the specification as an execution mechanism, because terms can grow exponentially with the number of $\beta$-steps. ... More
Crumbling Abstract MachinesJul 13 2019Extending the lambda-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing sharing points in between any two of them, reducing to the case where applications ... More
Statistical Epistemic LogicJul 13 2019We introduce a modal logic for describing statistical knowledge, which we call statistical epistemic logic. We propose a Kripke model dealing with probability distributions and stochastic assignments, and show a stochastic semantics for the logic. To ... More
Augmenting Neural Nets with Symbolic Synthesis: Applications to Few-Shot LearningJul 12 2019We propose symbolic learning as extensions to standard inductive learning models such as neural nets as a means to solve few shot learning problems. We device a class of visual discrimination puzzles that calls for recognizing objects and object relationships ... More
An Introduction to Abstract Classification Theory in the Operator Algebraic SettingJul 12 2019In the setting of modern mathematical logic and model theory, classification theory has been one of the landmark achievements of the field. Likewise, the classification of UHF-algebras and AF-algebras were substantial contributions to the field of operator ... More
Type Assignment for the Computational lambda-CalculusJul 12 2019We study polymorphic type assignment systems for untyped lambda-calculi with effects. We introduce an intersection type assignment system for Moggi's computational lambda-calculus, where a generic monad T is considered, and provide a concrete model of ... More
Intersection Types for the Computational lambda-CalculusJul 12 2019Jul 15 2019We study polymorphic type assignment systems for untyped lambda-calculi with effects. We introduce an intersection type assignment system for Moggi's computational lambda-calculus, where a generic monad T is considered, and provide models of the calculus ... More
Approximate Model Counting, Sparse XOR Constraints and Minimum DistanceJul 11 2019The problem of counting the number of models of a given Boolean formula has numerous applications, including computing the leakage of deterministic programs in Quantitative Information Flow. Model counting is a hard, #P-complete problem. For this reason, ... More
The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple FormulasJul 11 2019HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental ... More
From Hybrid Modal Logic to Matching Logic and backJul 11 2019Building on our previous work on hybrid polyadic modal logic we identify modal logic equivalents for Matching Logic, a logic for program specification and verification. This provides a rigorous way to transfer results between the two approaches, which ... More
ADDMC: Exact Weighted Model Counting with Algebraic Decision DiagramsJul 11 2019We compute exact literal-weighted model counts of CNF formulas. Our algorithm employs dynamic programming, with Algebraic Decision Diagrams as the primary data structure. This technique is implemented in ADDMC, a new model counter. We empirically evaluate ... More
The SAT+CAS Method for Combinatorial Search with Applications to Best MatricesJul 11 2019In this paper, we provide an overview of the SAT+CAS method that combines satisfiability checkers (SAT solvers) and computer algebra systems (CAS) to resolve combinatorial conjectures, and present new results vis-\`a-vis best matrices. The SAT+CAS method ... More
On the Complexity of Completing Binary PredicatesJul 10 2019Given a binary predicate P, the length of the smallest program that computes a complete extension of P is less than the size of the domain of P plus the amount of information that P has with the halting sequence. This result is derived from a theorem ... More
Differentiable Probabilistic Logic NetworksJul 10 2019Probabilistic logic reasoning is a central component of such cognitive architectures as OpenCog. However, as an integrative architecture, OpenCog facilitates cognitive synergy via hybridization of different inference methods. In this paper, we introduce ... More
The complexity of the first-order theory of pure equalityJul 10 2019We will find a lower bound on the recognition complexity of the theories that are nontrivial relative to equality (or equational-nontrivial), namely, each of these theories is consistent with the formula, whose sense is that there exist two various elements ... More
SAT Solvers and Computer Algebra Systems: A Powerful Combination for MathematicsJul 09 2019Over the last few decades, many distinct lines of research aimed at automating mathematics have been developed, including computer algebra systems (CASs) for mathematical modelling, automated theorem provers for first-order logic, SAT/SMT solvers aimed ... More
Symmetric Polymorphisms and Efficient Decidability of Promise CSPsJul 09 2019In the field of constraint satisfaction problems (CSP), promise CSPs are an exciting new direction of study. In a promise CSP, each constraint comes in two forms: "strict" and "weak," and in the associated decision problem one must distinguish between ... More
Making Study Populations Visible through Knowledge GraphsJul 09 2019Treatment recommendations within Clinical Practice Guidelines (CPGs) are largely based on findings from clinical trials and case studies, referred to here as research studies, that are often based on highly selective clinical populations, referred to ... More
solc-verify: A Modular Verifier for Solidity Smart ContractsJul 09 2019We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity ... More
Trustworthy Graph AlgorithmsJul 09 2019The goal of the LEDA project was to build an easy-to-use and extendable library of correct and efficient data structures, graph algorithms and geometric algorithms. We report on the use of formal program verification to achieve an even higher level of ... More
A duality theoretic view on limits of finite structuresJul 09 2019The study of limits of sequences of finite structures plays a crucial role in finite model theory. It is motivated by an attempt to understand the behaviour of dynamical systems, such as computer networks evolving over time. For this purpose, starting ... More
Handling localisation in rely/guarantee concurrency: An algebraic approachJul 09 2019The rely/guarantee approach of Jones extends Hoare logic with rely and guarantee conditions in order to allow compositional reasoning about shared-variable concurrent programs. This paper focuses on localisation in the context of rely/guarantee concurrency ... More
Proving Properties of Sorting Programs: A Case Study in Horn Clause VerificationJul 09 2019The proof of a program property can be reduced to the proof of satisfiability of a set of constrained Horn clauses (CHCs) which can be automatically generated from the program and the property. In this paper we have conducted a case study in Horn clause ... More
Ultimate TreeAutomizer (CHC-COMP Tool Description)Jul 09 2019We present Ultimate TreeAutomizer, a solver for satisfiability of sets of constrained Horn clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attractive properties in terms of expressiveness and accessibility to algorithmic ... More
Relational Verification via Invariant-Guided SynchronizationJul 09 2019Relational properties describe relationships that hold over multiple executions of one or more programs, such as functional equivalence. Conventional approaches for automatically verifying such properties typically rely on syntax-based, heuristic strategies ... More
On Quantitative Comparison of Chemical Reaction Network ModelsJul 09 2019Chemical reaction networks (CRNs) provide a convenient language for modelling a broad variety of biological systems. These models are commonly studied with respect to the time series they generate in deterministic or stochastic simulations. Their dynamic ... More
Characterising Probabilistic Alternating Simulation for Concurrent GamesJul 09 2019Probabilistic game structures combine both nondeterminism and stochasticity, where players repeatedly take actions simultaneously to move to the next state of the concurrent game. Probabilistic alternating simulation is an important tool to compare the ... More
Proof compression and NP versus PSPACE: AddendumJul 08 2019We upgrade [1] to a complete proof of the conjecture NP = PSPACE. [1]: L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE, Studia Logica (107) (1): 55-83 (2019)
$\unicode{8523}$ means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional ProgramsJul 08 2019Along the lines of the Abramsky ``Proofs-as-Processes'' program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multiple-conclusion natural deduction ... More
Bounded Model Checking of Max-Plus Linear Systems via Predicate AbstractionsJul 08 2019This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications under consideration. We focus on verifying time-difference specifications, ... More
Degrees of bi-embeddable categoricityJul 08 2019We investigate the complexity of embeddings between bi-embeddable structures. In analogy with categoricity spectra, we define the bi-embeddable categoricity spectrum of a structure $\mathcal A$ as the family of Turing degrees that compute embeddings between ... More
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational ReasoningJul 08 2019This volume contains the joint post-proceedings of the 3rd Workshop on Program Equivalence and Relational Reasoning (PERR) and the 6th Workshop on Horn Clauses for Verification and Synthesis (HCVS), which took place in Prague, Czech Republic on 6th and ... More
Polymorphism and the free bicartesian closed categoryJul 08 2019We study two decidable fragments of System F, the polynomial and the Yoneda fragment, inducing two representations of the free bicartesian closed category. The first fragment is freely generated by the encoding of finite polynomial functors (generalizing ... More
A Bridge Anchored on Both Sides: Formal Deduction in Introductory CS, and Code Proofs in Discrete MathJul 07 2019There is a sharp disconnect between the programming and mathematical portions of the standard undergraduate computer science curriculum, leading to student misunderstanding about how the two are related. We propose connecting the subjects early in the ... More
A Neutral Temporal Deontic STIT LogicJul 07 2019Jul 09 2019In this work we answer a long standing request for temporal embeddings of deontic STIT logics by introducing the multi-agent STIT logic TDS. The logic is based upon atemporal utilitarian STIT logic. Yet, the logic presented here will be neutral: instead ... More
Homogeneity of torsion-free hyperbolic groupsJul 07 2019We give a complete characterization of torsion-free hyperbolic groups which are homogeneous in the sense of first-order logic, in terms of the JSJ decompositions of their free factors.
Infinite monochromatic paths and a theorem of Erdos-Hajnal-RadoJul 07 2019We show that $\omega_1\nrightarrow_{\rm path}(\omega)^2_{\omega,<\omega}$ but $\omega_1\rightarrow_{\rm path}(\omega)^2_\omega$, whence we prove that if $\mu>{\rm cf}(\mu)=\omega$ and $2^\mu=\mu^+$ then $\binom{\mu^+}{\mu}\nrightarrow\binom{\mu^+\ \aleph_2}{\mu\ ... More
Universal One-Dimensional Cellular Automata Derived for Turing Machines and its Dynamical BehaviourJul 06 2019Universality in cellular automata theory is a central problem studied and developed from their origins by John von Neumann. In this paper, we present an algorithm where any Turing machine can be converted to one-dimensional cellular automaton with a 2-linear ... More
HTP-complete rings of rational numbersJul 06 2019For a ring $R$, Hilbert's Tenth Problem $HTP(R)$ is the set of polynomial equations over $R$, in several variables, with solutions in $R$. We view $HTP$ as an enumeration operator, mapping each set $W$ of prime numbers to $HTP(\mathbb Z[W^{-1}])$, which ... More
Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic LogicJul 05 2019Jul 08 2019Computer-Controlled Systems (CCS) are a subclass of hybrid systems where the periodic relation of control components to time is paramount. Since they additionally are at the heart of many safety-critical devices, it is of primary importance to correctly ... More
Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic LogicJul 05 2019Computer-Controlled Systems (CCS) are a subclass of hybrid systems where the periodic relation of control components to time is paramount. Since they additionally are at the heart of many safety-critical devices, it is of primary importance to correctly ... More
From LCF to Isabelle/HOLJul 05 2019Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search, borrowing techniques ... More
A comparison of various analytic choice principlesJul 05 2019We investigate computability theoretic and descriptive set theoretic contents of various kinds of analytic choice principles by performing detailed analysis of the Medvedev lattice of $\Sigma^1_1$-closed sets. Among others, we solve an open problem on ... More
Homogeneous Dual Ramsey TheoremJul 05 2019For positive integers $k < n$ such that $k$ divides $n$, let $(n)^k_{\hom}$ be the set of homogeneous $k$-partitions of $\{1, \dots, n\}$, that is, the set of partitions of $\{1, \dots, n\}$ into $k$ classes of the same cardinality. In the article "Ramsey ... More
Operational Semantics of GamesJul 05 2019We introduce operational semantics into games. And based on the operational semantics, we establish a full algebra of games, including basic algebra of games, algebra of concurrent games, recursion and abstraction. The algebra can be used widely to reason ... More
The Algebra of an Age for Metrically Homogeneous Graphs of Generic TypeJul 05 2019Metrically homogeneous graphs are connected graphs which, when endowed with the path metric, are homogeneous as metric spaces. Here we consider a class of countable metrically homogeneous graphs. The algebra of an age is a concept introduced by Cameron ... More
On Validating, Repairing and Refining Heuristic ML ExplanationsJul 04 2019Recent years have witnessed a fast-growing interest in computing explanations for Machine Learning (ML) models predictions. For non-interpretable ML models, the most commonly used approaches for computing explanations are heuristic in nature. In contrast, ... More
Revisiting local time semantics for networks of timed automataJul 04 2019We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks of timed automata working in parallel. In the timed setting this explosion ... More
A Formal Axiomatization of ComputationJul 04 2019We introduce a set of axioms for the notion of computation, and show that P= NP is not derivable from this set of axioms.
Lifting Datalog-based Analyses to Software Product LinesJul 04 2019Applying program analyses to Software Product Lines (SPLs) has been a fundamental research problem at the intersection of Product Line Engineering and software analysis. Different attempts have been made to "lift" particular product-level analyses to ... More
On Open-Universe Causal ReasoningJul 04 2019We extend two kinds of causal models, structural equation models and simulation models, to infinite variable spaces. This enables a semantics for conditionals founded on a calculus of intervention, and axiomatization of causal reasoning for rich, expressive ... More
The Combinatorics of Barrier SynchronizationJul 03 2019In this paper we study the notion of synchronization from the point of view of combinatorics. As a first step, we address the quantitative problem of counting the number of executions of simple processes interacting with synchronization barriers. We elaborate ... More
Computing Probabilistic Bisimilarity Distances for Probabilistic AutomataJul 03 2019Jul 04 2019The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity ... More
Computing Probabilistic Bisimilarity Distances for Probabilistic AutomataJul 03 2019The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity ... More
What's decidable about parametric timed automata?Jul 03 2019Parametric timed automata (PTAs) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After 25 years of research on PTAs, it is now well-understood that any non-trivial problem studied is undecidable for general ... More
Formalizing the Solution to the Cap Set ProblemJul 02 2019In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $\mathbb{F}^n_q$ with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case $q = 3$, where it is commonly ... More
Domain-Aware Session Types (Extended Version)Jul 02 2019We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, ... More
Specifying verified x86 software from scratchJul 02 2019We present a simple framework for specifying and proving facts about the input/output behavior of ELF binary files on the x86-64 architecture. A strong emphasis has been placed on simplicity at all levels: the specification says only what it needs to ... More
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)Jul 02 2019We give a linear nested sequent calculus for the basic normal tense logic Kt. We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut-elimination. Linear nested sequents thus provide the minimal amount of ... More
Timed Basic Parallel ProcessesJul 02 2019Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such ... More
Logics for Reversible Regular Languages and Semigroups with InvolutionJul 02 2019We present MSO and FO logics with predicates `between' and `neighbour' that characterise various fragments of the class of regular languages that are closed under the reverse operation. The standard connections that exist between MSO and FO logics and ... More
Core First Unit PropagationJul 02 2019Unit propagation (which is called also Boolean Constraint Propagation) has been an important component of every modern CDCL SAT solver since the CDCL solver was developed. In general, unit propagation is implemented by scanning sequentially every clause ... More
The Polynomial Complexity of Vector Addition Systems with StatesJul 01 2019Vector addition systems are an important model in theoretical computer science and have been used in a variety of areas. In this paper, we consider vector addition systems with states over a parameterized initial configuration. For these systems, we are ... More
Computing a Smaller Unit-Distance Graph with Chromatic Number 5 via Proof TrimmingJul 01 2019We present a method to gradually compute a smaller and smaller unsatisfiable core of a propositional formula by minimizing proofs of unsatisfiability. The goal is to compute a minimal unsatisfiable core that is relatively small compared to other minimal ... More
Trimming Graphs Using Clausal Proof OptimizationJul 01 2019Jul 15 2019We present a method to gradually compute a smaller and smaller unsatisfiable core of a propositional formula by minimizing proofs of unsatisfiability. The goal is to compute a minimal unsatisfiable core that is relatively small compared to other minimal ... More
Verifying that a compiler preserves concurrent value-dependent information-flow securityJul 01 2019It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when ... More
On Rudimentarity, Primitive Recursivity and RepresentabilityJul 01 2019It is quite well-known from Kurt G\"odel's (1931) ground-breaking result on the Incompleteness Theorem that rudimentary relations (i.e., those definable by bounded formulae) are primitive recursive, and that primitive recursive functions are representable ... More
Parametric Verification: An IntroductionJul 01 2019This paper constitutes a short introduction to parametric verification of concurrent systems. It originates from two 1-day tutorial sessions held at the Petri nets conferences in Toru\'n (2016) and Zaragoza (2017). The paper presents not only the basic ... More
A Formal Approach for Efficient Navigation Management of Hybrid Electric Vehicles on Long TripsJul 01 2019Plug-in Hybrid Electric Vehicles (PHEVs) are gaining popularity due to their economic efficiency as well as their contribution to green management. PHEVs allow the driver to use electric power exclusively for driving and then switch to gasoline as needed. ... More
Parametric Timed Model Checking for Guaranteeing Timed OpacityJul 01 2019Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on the system execution time. We address the ... More
Typed lambda-calculi and superclasses of regular functionsJun 30 2019We propose to use Church encodings in typed lambda-calculi as the basis for an automata-theoretic counterpart of implicit computational complexity, in the same way that monadic second-order logic provides a counterpart to descriptive complexity. Specifically, ... More
On countably saturated linear orders and certain class of countably saturated graphsJun 30 2019Countable saturation for linear orders is a natural strengthening of the notion of density. Study of countably saturated linear orders dates back as far as to Felix Hausdorff, who among others proved, that under CH all such orders of cardinality $\mathfrak{c}$ ... More
Upper bounds on the graph minor theoremJun 30 2019Lower bounds on the proof-theoretic strength of the graph minor theorem were found over 30 years ago by Friedman, Robertson and Seymour 1987, but upper bounds have always been elusive. We present recently found upper bounds on the graph minor theorem ... More
Rough conceptsJun 30 2019The present paper proposes a novel way to unify Rough Set Theory and Formal Concept Analysis. Our method stems from results and insights developed in the algebraic theory of modal logic, and is based on the idea that Pawlak's original approximation spaces ... More
Deciding Memory Safety for Forest DatastructuresJun 29 2019Memory safety is the problem of determining if a heap manipulating program that allocates/frees memory locations and manipulates heap pointers, does not dereference a memory location that is not allocated. Memory safety errors are serious security vulnerabilities ... More
Domain-Specific Language to Encode Induction HeuristicsJun 29 2019Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, they did not have a systematic way to encode their expertise. To address this problem, we present ... More
QCSP monsters and the demise of the Chen ConjectureJun 29 2019We give a surprising classification for the computational complexity of Quantified Constraint Satisfaction Problems, QCSP$(\Gamma)$, where $\Gamma$ is a finite language over $3$ elements which contains all constants. In particular, such problems are either ... More
Recursive axiomatizations from separation propertiesJun 29 2019We define a fragment of monadic infinitary second-order logic corresponding to a kind of abstract separation property. We use this to define certain subclasses of elementary classes as separation subclasses. We use model theoretic techniques and games ... More
DRAT-based Bit-Vector Proofs in CVC4Jun 28 2019Jul 02 2019Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for the theory of fixed-size bit-vectors employ an approach called bit-blasting, where a given formula is translated into a Boolean satisfiability (SAT) problem and delegated to a SAT ... More
Computing Haar MeasuresJun 28 2019According to Haar's Theorem, every compact group $G$ admits a unique left-invariant Borel probability measure $\mu_G$. Let the Haar integral (of $G$) denote the functional $\int_G:\mathcal{C}(G)\ni f\mapsto \int f\,d\mu_G$ integrating any continuous function ... More
Semantic expressive capacity with bounded memoryJun 27 2019We investigate the capacity of mechanisms for compositional semantic parsing to describe relations between sentences and semantic representations. We prove that in order to represent certain relations, mechanisms which are syntactically projective must ... More
A Game Model for Proofs with CostsJun 27 2019We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game, where player I defends a claim corresponding ... More
Dependency Pairs Termination in Dependent Type Theory Modulo RewritingJun 27 2019Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. ... More
Repairing Timed Automata Clock Guards through Abstraction and TestingJun 27 2019Timed automata (TAs) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, ... More
Finding Security Vulnerabilities in Unmanned Aerial Vehicles Using Software VerificationJun 27 2019The proliferation of Unmanned Aerial Vehicles (UAVs) embedded with vulnerable monolithic software, involving concurrency and fragile communication links, has recently raised serious concerns about their security. Recent studies show that a 2kg UAV can ... More
Truly Concurrent Bisimilarities are Game EquivalentJun 27 2019We design games for truly concurrent bisimilarities, including strongly truly concurrent bisimilarities and branching truly concurrent bisimilarities, such as pomset bisimilarities, step bisimilarities, history-preserving bisimilarities and hereditary ... More
Introducing Certified Compilation in Education by a Functional Language ApproachJun 27 2019Classes on compiler technology are commonly found in Computer Science curricula, covering aspects of parsing, semantic analysis, intermediate transformations and target code generation. This paper reports on introducing certified compilation techniques ... More
A Stricter Heap Separating Points-To LogicJun 26 2019Dynamic memory issues are hard to locate and may cost much of a development project's efforts and was repeatedly reported similarly afterwards independently by different persons. Verification as one formal method may proof a given program's heap matches ... More
First-order proofs without syntaxJun 26 2019Proofs are traditionally syntactic, inductively generated objects. This paper reformulates first-order logic (predicate calculus) with proofs which are graph-theoretic rather than syntactic. It defines a combinatorial proof of a formula $\phi$ as a lax ... More
On free completely iterative algebrasJun 26 2019Jun 27 2019For every finitary set functor F we demonstrate that free algebras carry a canonical partial order. In case F is bicontinuous, we prove that the cpo obtained as the conservative completion of the free algebra is the free completely iterative algebra. ... More
On free completely iterative algebrasJun 26 2019For every finitary set functor F we demonstrate that free algebras carry a canonical partial order. In case F is bicontinuous, we prove that the cpo obtained as the conservative completion of the free algebra is the free completely iterative algebra. ... More
Ilinva: Using Abduction to Generate Loop InvariantsJun 26 2019We describe a system to prove properties of programs. The key feature of this approach is a method to automatically synthesize inductive invariants of the loops contained in the program. The method is generic, i.e., it applies to a large set of programming ... More
A Computational Framework for Adaptive Systems and its VerificationJun 26 2019Modern computer systems are inherently distributed and feature autonomous and collaborative behaviour of multicomponent with global goals. These goals are expressed in terms of the combined behaviour of different components that are usually deployed in ... More
A unifying framework for continuity and complexity in higher typesJun 25 2019We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number of fundamental ... More
SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision ProcessesJun 25 2019For hybrid Markov decision processes, UPPAAL Stratego can compute strategies that are safe for a given safety property and (in the limit) optimal for a given cost function. Unfortunately, these strategies cannot be exported easily since they are computed ... More
Quantitative Verification of Neural Networks And its Security ApplicationsJun 25 2019Neural networks are increasingly employed in safety-critical domains. This has prompted interest in verifying or certifying logically encoded properties of neural networks. Prior work has largely focused on checking existential properties, wherein the ... More
Partial Quantifier Elimination With LearningJun 25 2019We consider a modification of the Quantifier Elimination (QE) problem called Partial QE (PQE). In PQE, only a small part of the formula is taken out of the scope of quantifiers. The appeal of PQE is that many verification problems, e.g. equivalence checking ... More
Datalog Materialisation in Distributed RDF Stores with Dynamic Data ExchangeJun 24 2019Several centralised RDF systems support datalog reasoning by precomputing and storing all logically implied triples using the wellknown seminaive algorithm. Large RDF datasets often exceed the capacity of centralised RDF systems, and a common solution ... More