We introduce a graphical syntax for signal flow diagrams based on the language of symmetric monoidal categories. Using universal categorical constructions, we provide a stream semantics and a sound and complete axiomatisation. A certain class of diagrams captures the orthodox notion of signal flow graph used in control theory; we show that any diagram of our syntax can be realised, via rewriting in the equational theory, as a signal flow graph.
We consider data automata in the form of finite automata equipped with variables (counters or registers) ranging over infinite data domains. A trace of such a data automaton is an alternating sequence of alphabet symbols and values taken by the counters during an execution of the automaton. We address the problem of checking the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable in general, we give a semi-algorithm based on abstraction refinement, which is proved to be sound and complete modulo termination. Due to the undecidability of the trace inclusion problem, our procedure is not guaranteed to terminate. We have implemented our technique in a prototype tool and show promising results on several non-trivial examples.
Unsatisfiability proofs in the DRAT format became the de
facto standard to increase the reliability of contemporary SAT solvers.
We consider the problem of generating proofs for the XOR reasoning
component in SAT solvers and propose two methods: direct translation
transforms every XOR constraint addition inference into a DRAT proof,
whereas T-translation avoids the exponential blow-up in direct transla-
tions by using fresh variables. T-translation produces DRAT proofs from
Gaussian elimination records that are polynomial in the size of the input
CNF formula. Experiments show that a combination of both approaches
with a simple prediction method outperforms the BDD-based method.
Security vulnerabilities plague modern systems because writing secure systems code is hard. Promising approaches can retrofit security automatically via runtime checks that implement the desired security policy; these checks guard critical operations, like memory accesses. Alas, the induced slowdown usually exceeds by a wide margin what system users are willing to tolerate in production, so these tools are hardly ever used. As a result, the insecurity of real-world systems persists. We present an approach in which developers/operators can specify what level of overhead they find acceptable for a given workload (e.g., 5%); our proposed tool ASAP then automatically instruments the program to maximize its security while staying within the specified “overhead budget.” Two insights make this approach effective: most overhead in existing tools is due to only a few “hot” checks, whereas the checks most useful to security are typically “cold”and cheap. We evaluate ASAP on programs from the Phoronix and SPEC benchmark suites. It can precisely select the best points in the security-performance spectrum. Moreover, we analyzed existing bugs and security vulnerabilities in RIPE, OpenSSL, and the Python interpreter, and found that the protection level offered by the ASAP approach is sufficient to protect against all of them. Joint work with Jonas Wagner, Volodymyr Kuznetsov and George Candea (EPFL), presented at IEEE S&P (Oakland) 2015.
Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of the form x ≤ y + c, and describe that the value of x in the current state is at most the value of y in the previous state plus some integer constant c. We believe that difference constraints are also a good choice for complexity and resource bound analysis because the complexity of imperative programs typically arises from counter increments and resets, which can be modeled naturally by difference constraints. In this article we propose a bound analysis based on difference constraints. We make the following contributions:
(1) Our analysis handles bound analysis problems of high practical relevance which current approaches cannot handle: We extend the range of bound analysis to a class of challenging but natural loop iteration patterns which typically appear in parsing and string-matching routines.
(2) We advocate the idea of using bound analysis to infer invariants: Our soundness proven algorithm obtains invariants through bound analysis, the inferred invariants are in turn used for obtaining bounds. Our bound analysis therefore does not rely on external techniques for invariant generation.
(3) We demonstrate that difference constraints are a suitable abstract program model for automatic complexity and resource bound analysis: We provide efficient abstraction techniques for obtaining difference constraint programs from imperative code.
(4) We report on a thorough experimental comparison of state-of-the-art bound analysis tools.