uu.seUppsala University Publications
Change search
Link to record
Permanent link

Direct link
BETA
Alternative names
Publications (10 of 46) Show all publications
Hong, C.-D., Lin, A. W., Majumdar, R. & Rümmer, P. (2019). Probabilistic Bisimulation for Parameterized Systems: (with Applications to Verifying Anonymous Protocols). In: Computer Aided Verification. CAV 2019.: . Paper presented at 31st International Conference on Computer-Aided Verification, July 13-18, 2019, New York City, US. (pp. 455-474). Cham, 11561
Open this publication in new window or tab >>Probabilistic Bisimulation for Parameterized Systems: (with Applications to Verifying Anonymous Protocols)
2019 (English)In: Computer Aided Verification. CAV 2019., Cham, 2019, Vol. 11561, p. 455-474Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Cham: , 2019
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-398241 (URN)10.1007/978-3-030-25540-4_27 (DOI)000491468000027 ()978-3-030-25539-8 (ISBN)978-3-030-25540-4 (ISBN)
Conference
31st International Conference on Computer-Aided Verification, July 13-18, 2019, New York City, US.
Funder
Swedish Research Council, 2018-04727Swedish Foundation for Strategic Research , RIT17-0011EU, European Research Council, 759969EU, European Research Council, 610150German Research Foundation (DFG), 389792660-TRR 248
Available from: 2019-12-04 Created: 2019-12-04 Last updated: 2019-12-06Bibliographically approved
Klebanov, V., Rümmer, P. & Ulbrich, M. (2018). Automating regression verification of pointer programs by predicate abstraction. Formal methods in system design, 52(3), 229-259
Open this publication in new window or tab >>Automating regression verification of pointer programs by predicate abstraction
2018 (English)In: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 52, no 3, p. 229-259Article in journal (Refereed) Published
Abstract [en]

Regression verification is an approach complementing regression testing with formal verification. The goal is to formally prove that two versions of a program behave either equally or differently in a precisely specified way. In this paper, we present a novel automated approach for regression verification that reduces the equivalence of two related imperative pointer programs to constrained Horn clauses over uninterpreted predicates. Subsequently, state-of-the-art SMT solvers are used to solve the clauses. We have implemented the approach, and our experiments show that non-trivial programs with integer and pointer arithmetic can now be proved equivalent without further user input.

Keywords
Regression verification, Horn constraint solving, Program equivalence, Relational program verification
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-356860 (URN)10.1007/s10703-017-0293-8 (DOI)000431870700002 ()
Funder
Swedish Research Council, 2014-5484
Available from: 2018-08-15 Created: 2018-08-15 Last updated: 2018-12-07Bibliographically approved
Backeman, P., Rümmer, P. & Zeljic, A. (2018). Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction. In: Nikolaj Bjørner, Arie Gurfinkel (Ed.), Formal Methods in Computer-Aided Design: . Paper presented at The eighteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification (FMCAD 2018), 30 October - 2 November, 2018, University of Texas, Austin, Texas. (pp. 50-59). IEEE
Open this publication in new window or tab >>Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
2018 (English)In: Formal Methods in Computer-Aided Design / [ed] Nikolaj Bjørner, Arie Gurfinkel, IEEE, 2018, p. 50-59Conference paper, Published paper (Refereed)
Abstract [en]

The inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bitvector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider

Place, publisher, year, edition, pages
IEEE, 2018
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-368030 (URN)10.23919/FMCAD.2018.8603023 (DOI)000493916300012 ()978-0-9835678-8-2 (ISBN)
Conference
The eighteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification (FMCAD 2018), 30 October - 2 November, 2018, University of Texas, Austin, Texas.
Funder
Swedish Research Council, 2014-5484Swedish Foundation for Strategic Research , RIT17-0011
Available from: 2018-12-04 Created: 2018-12-04 Last updated: 2019-12-06Bibliographically approved
Zeljic, A., Backeman, P., Wintersteiger, C. M. & Rümmer, P. (2018). Exploring Approximations for Floating-Point Arithmetic using UppSAT. In: Didier Galmiche, Stephan Schulz, Roberto Sebastiani (Ed.), Automated Reasoning: . Paper presented at 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018 (pp. 246-262). Springer
Open this publication in new window or tab >>Exploring Approximations for Floating-Point Arithmetic using UppSAT
2018 (English)In: Automated Reasoning / [ed] Didier Galmiche, Stephan Schulz, Roberto Sebastiani, Springer, 2018, p. 246-262Conference paper, Published paper (Refereed)
Abstract [en]

We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT—an new implementation of a systematic approximation refinement framework as an abstract SMT solver. Provided with an approximation and a decision procedure (implemented in an off-the-shelf SMT solver), UppSAT yields an approximating SMT solver. Additionally, UppSAT includes a library of predefined approximation components which can be combined and extended to define new encodings, orderings and solving strategies. We propose that UppSAT can be used as a sandbox for easy and flexible exploration of new approximations. To substantiate this, we explore encodings of floating-point arithmetic into reduced precision floating-point arithmetic, real-arithmetic, and fixed-point arithmetic (encoded into the theory of bit-vectors in practice). In an experimental evaluation we compare the advantages and disadvantages of approximating solvers obtained by combining various encodings and decision procedures.

Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10900
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-368468 (URN)10.1007/978-3-319-94205-6_17 (DOI)000470004600017 ()978-3-319-94204-9 (ISBN)978-3-319-94205-6 (ISBN)
Conference
9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018
Funder
Swedish Research Council, 2014-5484
Available from: 2018-12-04 Created: 2018-12-04 Last updated: 2019-06-26Bibliographically approved
Holik, L., Janku, P., Lin, A. W., Rümmer, P. & Vojnar, T. (2018). String constraints with concatenation and transducers solved efficiently. Paper presented at Principles of Programming Languages 2018. Proceedings of the ACM on Programming Languages, 2, 1-32, Article ID 4.
Open this publication in new window or tab >>String constraints with concatenation and transducers solved efficiently
Show others...
2018 (English)In: Proceedings of the ACM on Programming Languages, E-ISSN 2475-1421, Vol. 2, p. 1-32, article id 4Article in journal (Refereed) Published
Abstract [en]

String analysis is the problem of reasoning about how strings are manipulated by a program. It has numerous applications including automatic detection of cross-site scripting, and automatic test-case generation. A popular string analysis technique includes symbolic executions, which at their core use constraint solvers over the string domain, a.k.a. string solvers. Such solvers typically reason about constraints expressed in theories over strings with the concatenation operator as an atomic constraint. In recent years, researchers started to recognise the importance of incorporating the replace-all operator (i.e. replace all occurrences of a string by another string) and, more generally, finite-state transductions in the theories of strings with concatenation. Such string operations are typically crucial for reasoning about XSS vulnerabilities in web applications, especially for modelling sanitisation functions and implicit browser transductions (e.g. innerHTML). Although this results in an undecidable theory in general, it was recently shown that the straight-line fragment of the theory is decidable, and is sufficiently expressive in practice. In this paper, we provide the first string solver that can reason about constraints involving both concatenation and finite-state transductions. Moreover, it has a completeness and termination guarantee for several important fragments (e.g. straight-line fragment). The main challenge addressed in the paper is the prohibitive worst-case complexity of the theory (double-exponential time), which is exponentially harder than the case without finite-state transductions. To this end, we propose a method that exploits succinct alternating finite-state automata as concise symbolic representations of string constraints. In contrast to previous approaches using nondeterministic automata, alternation offers not only exponential savings in space when representing Boolean combinations of transducers, but also a possibility of succinct representation of otherwise costly combinations of transducers and concatenation. Reasoning about the emptiness of the AFA language requires a state-space exploration in an exponential-sized graph, for which we use model checking algorithms (e.g. IC3). We have implemented our algorithm and demonstrated its efficacy on benchmarks that are derived from cross-site scripting analysis and other examples in the literature.

Place, publisher, year, edition, pages
New York: ACM Digital Library, 2018
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-368719 (URN)10.1145/3158092 (DOI)
Conference
Principles of Programming Languages 2018
Funder
Swedish Research Council, 2014-5484
Available from: 2018-12-06 Created: 2018-12-06 Last updated: 2018-12-14Bibliographically approved
Hojjat, H. & Rümmer, P. (2018). The ELDARICA Horn Solver. In: Formal Methods in Computer Aided Design: . Paper presented at The eighteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification (FMCAD 2018), 30 October - 2 November, 2018, University of Texas, Austin, Texas. (pp. 158-164). IEEE
Open this publication in new window or tab >>The ELDARICA Horn Solver
2018 (English)In: Formal Methods in Computer Aided Design, IEEE, 2018, p. 158-164Conference paper, Published paper (Refereed)
Abstract [en]

This paper presents the ELDARICA version 2 model checker. Over the last years we have been developing and maintaining ELDARICA as a state-of-the-art solver for Horn clauses over integer arithmetic. In the version 2, we have extended the solver to support also algebraic data types and bit-vectors, theories that are commonly applied in verification, but currently unsupported by most Horn solvers. This paper describes the high-level structure of the tool and the interface that it provides to other applications. We also report on an evaluation of the tool. While some of the techniques in ELDARICA have been documented in research papers over the last years, this is the first tool paper describing ELDARICA in its entirety.

Place, publisher, year, edition, pages
IEEE, 2018
National Category
Computer Sciences
Research subject
Computing Science
Identifiers
urn:nbn:se:uu:diva-368717 (URN)10.23919/FMCAD.2018.8603013 (DOI)000493916300024 ()978-0-9835678-8-2 (ISBN)
Conference
The eighteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification (FMCAD 2018), 30 October - 2 November, 2018, University of Texas, Austin, Texas.
Funder
Swedish Research Council, 2014-5484Swedish Foundation for Strategic Research , RIT17-0011
Available from: 2018-12-06 Created: 2018-12-06 Last updated: 2019-12-06Bibliographically approved
Abdulla, P. A., Atig, M. F., Chen, Y.-F., Bui, P. D., Holik, L., Rezine, A. & Rümmer, P. (2018). Trau: SMT solver for string constraints. In: Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD): . Paper presented at 18th Conference on Formal Methods in Computer-Aided Design (FMCAD), October 30-November 2, 2018, Austin, USA. IEEE
Open this publication in new window or tab >>Trau: SMT solver for string constraints
Show others...
2018 (English)In: Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD), IEEE, 2018Conference paper, Published paper (Refereed)
Abstract [en]

We introduce TRAU, an SMT solver for an expressive constraint language, including word equations, length constraints, context-free membership queries, and transducer constraints. The satisfiability problem for such a class of constraints is in general undecidable. The key idea behind TRAU is a technique called flattening, which searches for satisfying assignments that follow simple patterns. TRAU implements a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The approximations are refined in an automatic manner by information flow between the two modules. The technique implemented by TRAU can handle a rich class of string constraints and has better performance than state-of-the-art string solvers.

Place, publisher, year, edition, pages
IEEE, 2018
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-367967 (URN)10.23919/FMCAD.2018.8602997 (DOI)000493916300025 ()978-0-9835678-8-2 (ISBN)
Conference
18th Conference on Formal Methods in Computer-Aided Design (FMCAD), October 30-November 2, 2018, Austin, USA
Funder
Swedish Research Council, 2014-5484Swedish Foundation for Strategic Research , RIT17-0011
Available from: 2018-11-30 Created: 2018-11-30 Last updated: 2019-12-06Bibliographically approved
Piskac, R. & Rümmer, P. (Eds.). (2018). Verified Software. Theories, Tools, and Experiments: Revised Selected Papers. Paper presented at Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE, Oxford, UK, 2018. Springer Publishing Company
Open this publication in new window or tab >>Verified Software. Theories, Tools, and Experiments: Revised Selected Papers
2018 (English)Conference proceedings (editor) (Refereed)
Place, publisher, year, edition, pages
Springer Publishing Company, 2018. p. 345
Series
Lecture Notes in Computer Science ; 11294
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-368724 (URN)978-3-030-03591-4 (ISBN)
Conference
Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE, Oxford, UK, 2018
Available from: 2018-12-06 Created: 2018-12-06 Last updated: 2019-04-25Bibliographically approved
Zeljic, A., Wintersteiger, C. M. & Rümmer, P. (2017). An approximation framework for solvers and decision procedures. Journal of automated reasoning, 58(1), 127-147
Open this publication in new window or tab >>An approximation framework for solvers and decision procedures
2017 (English)In: Journal of automated reasoning, ISSN 0168-7433, E-ISSN 1573-0670, Vol. 58, no 1, p. 127-147Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-305180 (URN)10.1007/s10817-016-9393-1 (DOI)000392387400006 ()
Projects
UPMARC
Available from: 2016-11-10 Created: 2016-10-12 Last updated: 2018-01-14Bibliographically approved
Lengál, O., Lin, A. W., Majumdar, R. & Rümmer, P. (2017). Fair termination for parameterized probabilistic concurrent systems. In: Tools and Algorithms for the Construction and Analysis of Systems: Part I. Paper presented at 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2017, April 22–29, Uppsala, Sweden (pp. 499-517). Springer
Open this publication in new window or tab >>Fair termination for parameterized probabilistic concurrent systems
2017 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: Part I, Springer, 2017, p. 499-517Conference paper, Published paper (Refereed)
Abstract [en]

We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinite-state system: for each number n, the family consists of an instance with n finite-state processes. In contrast to safety, the parameterized verification of liveness is currently still considered extremely challenging especially in the presence of probabilities in the model. One major challenge is to provide a sufficiently powerful symbolic framework. One well-known symbolic framework for the parameterized verification of non-probabilistic concurrent systems is regular model checking. Although the framework was recently extended to probabilistic systems, incorporating fairness in the framework-often crucial for verifying termination-has been especially difficult due to the presence of an infinite number of fairness constraints (one for each process). Our main contribution is a systematic, regularity-preserving, encoding of finitary fairness (a realistic notion of fairness proposed by Alur and Henzinger) in the framework of regular model checking for probabilistic parameterized systems. Our encoding reduces termination with finitary fairness to verifying parameterized termination without fairness over probabilistic systems in regular model checking (for which a verification framework already exists). We show that our algorithm could verify termination for many interesting examples from distributed algorithms (Herman's protocol) and evolutionary biology (Moran process, cell cycle switch), which do not hold under the standard notion of fairness. To the best of our knowledge, our algorithm is the first fully-automatic method that can prove termination for these examples.

Place, publisher, year, edition, pages
Springer, 2017
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10205
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-337240 (URN)10.1007/978-3-662-54577-5_29 (DOI)000440734900029 ()978-3-662-54576-8 (ISBN)
Conference
23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2017, April 22–29, Uppsala, Sweden
Funder
Swedish Research Council, 2014-5484EU, European Research Council, 610150
Available from: 2017-03-31 Created: 2017-12-21 Last updated: 2018-11-19Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-2733-7098

Search in DiVA

Show all publications