| 1. |
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
- 2013
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin Heidelberg.
-
Konferensbidrag (refereegranskat)abstract
- We present a technique for automatically verifying safety properties of concurrent programs, in particular programs which rely on subtle dependen- cies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded num- ber of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state au- tomata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verifica- tion, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have imple- mented our method and used it to verify programs, some of which have not been verified by any other automatic method before.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Block me if you can! : Context-sensitive parameterized verification
- 2014
-
Ingår i: Static Analysis. - Cham : Springer. - 9783319109350 ; , s. 1-17
-
Konferensbidrag (refereegranskat)abstract
- We present a method for automatic verification of systems with a parameterized number of communicating processes, such as mutual exclusion protocols or agreement protocols. To that end, we present a powerful abstraction framework that uses an efficient and precise symbolic encoding of (infinite) sets of configurations. In particular, it generalizes downward-closed sets that have successfully been used in earlier approaches to parameterized verification. We show experimentally the efficiency of the method, on various examples, including a fine-grained model of Szymanski’s mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.
|
|
| 6. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Chain-Free String Constraints
- 2019
-
Ingår i: Automated Technology for Verification and Analysis. - Cham : Springer. - 9783030317836 - 9783030317843 ; , s. 277-293
-
Konferensbidrag (refereegranskat)abstract
- We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable fragment of string constraints, called weakly chaining string constraints, for which we show that the satisfiability problem is decidable. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. We have developed a prototype implementation of our new decision procedure, and integrated it into in an existing framework that uses CEGAR with under-approximation of string constraints based on flattening. Our experimental results show the competitiveness and accuracy of the new framework.
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Composed Bisimulation for Tree Automata
- 2008
-
Ingår i: Implementation and Application of Automata. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783540708438 ; , s. 212-222
-
Konferensbidrag (refereegranskat)
|
|
| 8. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Composed bisimulation for tree automata
- 2009
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 20:4, s. 685-700
-
Tidskriftsartikel (refereegranskat)
|
|
| 9. |
|
|
| 10. |
|
|
| 11. |
- Abdulla, Parosh Aziz, 1961-, et al.
(författare)
-
Flatten and Conquer : A Framework for Efficient Analysis of String Constraints
- 2017
-
Ingår i: SIGPLAN notices. - New York, NY, USA : ACM. - 0362-1340 .- 1558-1160. - 9781450349888 ; 52:6, s. 602-617, s. 602-617
-
Tidskriftsartikel (refereegranskat)abstract
- We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under-and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.
|
|
| 12. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Norn: An SMT Solver for String Constraints
- 2015
-
Ingår i: COMPUTER AIDED VERIFICATION, PT I. - Cham : SPRINGER-VERLAG BERLIN. - 9783319216904 - 9783319216898 ; , s. 462-469
-
Konferensbidrag (refereegranskat)abstract
- We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.
|
|
| 13. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Parameterized verification through view abstraction
- 2016
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 18:5, s. 495-516
-
Tidskriftsartikel (refereegranskat)abstract
- We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.
|
|
| 14. |
|
|
| 15. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
String Constraints for Verification
- 2014
-
Ingår i: <em>26th International Conference on Computer Aided Verification (CAV 2014), Vienna, Austria, Jul. 9-12, 2014.</em>. - Berlin : Springer. - 9783319088662 - 9783319088679 ; , s. 150-166
-
Konferensbidrag (refereegranskat)abstract
- We present a decision procedure for a logic that combines (i) word equations over string variables denoting words of arbitrary lengths, together with (ii) constraints on the length of words, and on (iii) the regular languages to which words belong. Decidability of this general logic is still open. Our procedure is sound for the general logic, and a decision procedure for a particularly rich fragment that restricts the form in which word equations are written. In contrast to many existing procedures, our method does not make assumptions about the maximum length of words. We have developed a prototypical implementation of our decision procedure, and integrated it into a CEGAR-based model checker for the analysis of programs encoded as Horn clauses. Our tool is able to automatically establish the correctness of several programs that are beyond the reach of existing methods.
|
|
| 16. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
String Constraints for Verification
- 2014
-
Ingår i: Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings. - Cham : Springer. - 9783319088662 ; , s. 150-166
-
Konferensbidrag (refereegranskat)abstract
- We present a decision procedure for a logic that combines (i) word equations over string variables denoting words of arbitrary lengths, together with (ii) constraints on the length of words, and on (iii) the regular languages to which words belong. Decidability of this general logic is still open. Our procedure is sound for the general logic, and a decision procedure for a particularly rich fragment that restricts the form in which word equations are written. In contrast to many existing procedures, our method does not make assumptions about the maximum length of words. We have developed a prototypical implementation of our decision procedure, and integrated it into a CEGAR-based model checker for the analysis of programs encoded as Horn clauses. Our tool is able to automatically establish the correctness of several programs that are beyond the reach of existing methods.
|
|
| 17. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
TRAU : SMT solver for string constraints
- 2018
-
Ingår i: PROCEEDINGS OF THE 2018 18TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD). - : IEEE. - 9780983567882 ; , s. 165-169
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 18. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Verification of heap manipulating programs with ordered data by extended forest automata
- 2016
-
Ingår i: Acta Informatica. - : Springer Science and Business Media LLC. - 0001-5903 .- 1432-0525. ; 53:4, s. 357-385
-
Tidskriftsartikel (refereegranskat)abstract
- We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.
|
|
| 19. |
|
|
| 20. |
|
|
| 21. |
- Abdulla, Parosh, 1961-, et al.
(författare)
-
An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures
- 2017
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 19:5, s. 549-563
-
Tidskriftsartikel (refereegranskat)abstract
- We present a technique for automatically verifying safety properties of concurrent programs, in particular programs that rely on subtle dependencies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded number of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state automata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verification, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have implemented our method and used it to verify programs, some of which have not been verified by any other automatic method before.
|
|
| 22. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Efficient Handling of String-Number Conversion
- 2020
-
Ingår i: PLDI 2020. - New York, NY, USA : ACM. - 9781450376136 ; , s. 943-957
-
Konferensbidrag (refereegranskat)abstract
- String-number conversion is an important class of constraints needed for the symbolic execution of string-manipulating programs. In particular solving string constraints with string-number conversion is necessary for the analysis of scripting languages such as JavaScript and Python, where string-number conversion is a part of the definition of the core semantics of these languages. However, solving this type of constraint is very challenging for the state-of-the-art solvers. We propose in this paper an approach that can efficiently support both string-number conversion and other common types of string constraints. Experimental results show that it significantly outperforms other state-of-the-art tools on benchmarks that involves string-number conversion.
|
|
| 23. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Solving Not-Substring Constraint with Flat Abstraction
- 2021
-
Ingår i: Programming Languages And Systems, APLAS 2021. - Cham : Springer Nature. - 9783030890513 - 9783030890506 ; , s. 305-320
-
Konferensbidrag (refereegranskat)abstract
- Not-substring is currently among the least supported types of string constraints, and existing solvers use only relatively crude heuristics. Yet, not-substring occurs relatively often in practical examples and is useful in encoding other types of constraints. In this paper, we propose a systematic way to solve not-substring using based on flat abstraction. In this framework, the domain of string variables is restricted to flat languages and subsequently the whole constraints can be expressed as linear arithmetic formulae. We show that non-substring constraints can be flattened efficiently, and provide experimental evidence that the proposed solution for not-substring is competitive with the state of the art string solvers.
|
|
| 24. |
- Aziz Abdulla, Parosh, et al.
(författare)
-
An integrated specification and verification technique for highly concurrent data structures
- 2017
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 19:5, s. 549-563
-
Tidskriftsartikel (refereegranskat)abstract
- We present a technique for automatically verifying safety properties of concurrent programs, in particular programs that rely on subtle dependencies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded number of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state automata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verification, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have implemented our method and used it to verify programs, some of which have not been verified by any other automatic method before.
|
|
| 25. |
- Habermehl, Peter, et al.
(författare)
-
Forest automata for verification of heap manipulation
- 2012
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 41:1, s. 83-106
-
Tidskriftsartikel (refereegranskat)abstract
- We consider verification of programs manipulating dynamic linked data structures such as various forms of singly and doubly-linked lists or trees. We consider important properties for this kind of systems like no null-pointer dereferences, absence of garbage, shape properties, etc. We develop a verification method based on a novel use of tree automata to represent heap configurations. A heap is split into several "separated" parts such that each of them can be represented by a tree automaton. The automata can refer to each other allowing the different parts of the heaps to mutually refer to their boundaries. Moreover, we allow for a hierarchical representation of heaps by allowing alphabets of the tree automata to contain other, nested tree automata. Program instructions can be easily encoded as operations on our representation structure. This allows verification of programs based on symbolic state-space exploration together with refinable abstraction within the so-called abstract regular tree model checking. A motivation for the approach is to combine advantages of automata-based approaches (higher generality and flexibility of the abstraction) with some advantages of separation-logic-based approaches (efficiency). We have implemented our approach and tested it successfully on multiple non-trivial case studies.
|
|
| 26. |
- Haziza, Frédéric, et al.
(författare)
-
Pointer Race Freedom
- 2016
-
Ingår i: Verification, Model Checking, And Abstract Interpretation, VMCAI 2016. - Berlin, Heidelberg : Springer. - 9783662491225 - 9783662491218 ; , s. 393-412
-
Konferensbidrag (refereegranskat)abstract
- We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessor's control whether or not the cell has been re-allocated. We establish two results. (1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection. (2) Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speedup of up to two orders of magnitude.
|
|
| 27. |
- Holik, Lukás, et al.
(författare)
-
Mediator synthesis in a component algebra with data
- 2015
-
Ingår i: Correct System Design. - Cham : Springer. - 9783319235059 ; , s. 238-259
-
Konferensbidrag (refereegranskat)abstract
- We formulate a compositional specification theory for components that interact by directed synchronous communication actions. The theory is an extension of interface automata which is also able to capture both absence of deadlock as well as constraints on data parameters in interactions. We define refinement, parallel composition, and quotient. The quotient is an adjoint of parallel composition, and produces the most general component that makes the components cooperate to satisfy a given system specification. We show how these operations can be used to synthesize mediators that allow components in networked systems to interoperate. This is illustrated by application to the synthesis of mediators in e-commerce applications.
|
|
| 28. |
- Holik, Lukas, et al.
(författare)
-
String constraints with concatenation and transducers solved efficiently
- 2018
-
Ingår i: Proceedings of the ACM on Programming Languages. - New York : ACM Digital Library. - 2475-1421. ; 2:POPL, s. 1-32
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
