liu.seSearch for publications in DiVA
Change search
Link to record
Permanent link

Direct link
BETA
Rezine, Ahmed
Publications (10 of 17) Show all publications
Ganjei, Z., Rezine, A., Eles, P. & Peng, Z. (2016). Counting dynamically synchronizing processes. International Journal on Software Tools for Technology Transfer (STTT), 18(5), 517-534
Open this publication in new window or tab >>Counting dynamically synchronizing processes
2016 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, no 5, p. 517-534Article in journal (Refereed) Published
Abstract [en]

We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared variables to count and synchronize the spawned processes. This allows them to implement intricate synchronization mechanisms, such as barriers. Automatically verifying correctness, and deadlock freedom, of such programs is beyond the capabilities of current techniques. For this purpose, we make use of counting predicates that mix counters referring to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build a nested counter example based refinement scheme for establishing correctness (expressed as non-reachability of configurations satisfying counting predicates formulas). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification on several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016
Keywords
Parameterized verification, Counting predicate, Barrier synchronization, Deadlock freedom, Multithreaded programs, Counter abstraction, Predicate abstraction, Constrained monotonic abstraction
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-124406 (URN)10.1007/s10009-015-0411-0 (DOI)000382011100004 ()
Note

Funding agencies: 12.04 CENIIT project

Available from: 2016-01-28 Created: 2016-01-28 Last updated: 2018-01-10
Ganjei, Z., Rezine, A., Eles, P. & Peng, Z. (2016). Lazy Constrained Monotonic Abstraction. In: Barbara Jobstmann; K. Rustan M. Leino (Ed.), Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Paper presented at 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016 (pp. 147-165). Springer Berlin/Heidelberg, 9583
Open this publication in new window or tab >>Lazy Constrained Monotonic Abstraction
2016 (English)In: Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings / [ed] Barbara Jobstmann; K. Rustan M. Leino, Springer Berlin/Heidelberg, 2016, Vol. 9583, p. 147-165Conference paper, Published paper (Refereed)
Abstract [en]

We introduce Lazy Constrained Monotonic Abstraction (lazy CMA for short) for lazily and soundly exploring well structured abstractions of infinite state non-monotonic systems. CMA makes use of infinite state and well structured abstractions by forcing monotonicity wrt. refinable orderings. The new orderings can be refined based on obtained false positives in a CEGAR like fashion. This allows for the verification of systems that are not monotonic and are hence inherently beyond the reach of classical analysis based on the theory of well structured systems. In this paper, we consistently improve on the existing approach by localizing refinements and by avoiding to trash the explored state space each time a refinement step is required for the ordering. To this end, we adapt ideas from classical lazy predicate abstraction and explain how we address the fact that the number of control points (i.e., minimal elements to be visited) is a priori unbounded. This is unlike the case of plain lazy abstraction which relies on the fact that the number of control locations is finite. We propose several heuristics and report on our experiments using our open source prototype. We consider both backward and forward explorations on non-monotonic systems automatically derived from concurrent programs. Intuitively, the approach could be regarded as using refinable upward closure operators as localized widening operators for an a priori arbitrary number of control points.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349
Keywords
Constrained monotonic abstraction, Lazy exploration, Well structured systems, Safety properties, Counter machines reachability
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-123739 (URN)10.1007/978-3-662-49122-5_7 (DOI)000375148800007 ()9783662491218 (ISBN)9783662491225 (ISBN)
Conference
17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016
Available from: 2016-01-11 Created: 2016-01-11 Last updated: 2018-02-06Bibliographically approved
Ganjei, Z., Rezine, A., Ion Eles, P. & Peng, Z. (2015). Abstracting and Counting Synchronizing Processes. In: Verification, Model Checking, and Abstract Interpretation: 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015.. Paper presented at VMCAI 15 (pp. 227-244). Springer
Open this publication in new window or tab >>Abstracting and Counting Synchronizing Processes
2015 (English)In: Verification, Model Checking, and Abstract Interpretation: 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015., Springer, 2015, p. 227-244Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. Automatically checking such properties for these programs is beyond the capabilities of current verification techniques. For this purpose, we describe an original logic that mixes two sorts of variables: those shared and manipulated by the concurrent processes, and ghost variables referring to the number of processes satisfying predicates on shared and local program variables. We then combine existing works on counter, predicate, and constrained monotonic abstraction and nest two cooperating counter example based refinement loops for establishing correctness (safety expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of synchronizing processes.

Place, publisher, year, edition, pages
Springer, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8931
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:liu:diva-114467 (URN)10.1007/978-3-662-46081-8_13 (DOI)000354784200013 ()978-3-662-46080-1 (ISBN)978-3-662-46081-8 (ISBN)
Conference
VMCAI 15
Available from: 2015-02-20 Created: 2015-02-20 Last updated: 2018-01-11
Aziz Abdulla, P., Faouzi Atig, M., Chen, Y.-F., Holik, L., Rezine, A., Rummer, P. & Stenman, J. (2015). Norn: An SMT Solver for String Constraints. In: Kroening, Daniel, Păsăreanu, Corina S. (Ed.), COMPUTER AIDED VERIFICATION, PT I: . Paper presented at 27th International Conference on Computer-Aided Verification (CAV) (pp. 462-469). SPRINGER-VERLAG BERLIN, 9206
Open this publication in new window or tab >>Norn: An SMT Solver for String Constraints
Show others...
2015 (English)In: COMPUTER AIDED VERIFICATION, PT I / [ed] Kroening, Daniel, Păsăreanu, Corina S., SPRINGER-VERLAG BERLIN , 2015, Vol. 9206, p. 462-469Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
SPRINGER-VERLAG BERLIN, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 9206
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:liu:diva-123090 (URN)10.1007/978-3-319-21690-4_29 (DOI)000364182900029 ()978-3-319-21690-4 (ISBN)978-3-319-21689-8 (ISBN)
Conference
27th International Conference on Computer-Aided Verification (CAV)
Available from: 2015-12-03 Created: 2015-12-03 Last updated: 2018-02-15
Abdulla, P. A., Atig, M. F., Ganjei, Z., Rezine, A. & Zhu, Y. (2015). Verification of Cache Coherence Protocols wrt. Trace Filters. In: : . Paper presented at Formal Methods in Computer-Aided Design (FMCAD). IEEE
Open this publication in new window or tab >>Verification of Cache Coherence Protocols wrt. Trace Filters
Show others...
2015 (English)Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of parameterized verification of cache coherence protocols for hardware accelerated transactional memories. In this setting, transactional memories leverage on the versioning capabilities of the underlying cache coherence protocol. The length of the transactions, their number, and the number of manipulated variables (i.e., cache lines) are parameters of the verification problem. Caches in such systems are finite-state automata communicating via broadcasts and shared variables. We augment our system with filters that restrict the set of possible executable traces according to existing conflict resolution policies. We show that the verification of coherence for parameterized cache protocols with filters can be reduced to systems with only a finite number of cache lines. For verification, we show how to account for the effect of the adopted filters in a symbolic backward reachability algorithm based on the framework of constrained monotonic abstraction. We have implemented our method and used it to verify transactional memory coherence protocols with respect to different conflict resolution policies.

Place, publisher, year, edition, pages
IEEE, 2015
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-128860 (URN)9780983567851 (ISBN)
Conference
Formal Methods in Computer-Aided Design (FMCAD)
Available from: 2016-06-02 Created: 2016-06-02 Last updated: 2018-01-10
Ganjei, Z., Rezine, A., Eles, P. & Peng, Z. (2014). Abstracting and Counting Synchronizing Processes.
Open this publication in new window or tab >>Abstracting and Counting Synchronizing Processes
2014 (English)Report (Other academic)
Abstract [en]

We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. Automatically checking such properties for these programs is beyond the capabilities of current verification techniques. For this purpose, we describe an original logic that mixes two sorts of variables: those shared and manipulated by the concurrent processes, and ghost variables refering to the number of processes satisfying predicates on shared and local program variables. We then combine existing works on counter, predicate, and constrained monotonic abstraction and nest two cooperating counter example based refinement loops for establishing correctness (safety expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of synchronizing processes. 

Publisher
p. 35
Series
Technical reports in Computer and Information Science, ISSN 1654-7233
Keywords
Parameterized verification, counting logic, barrier synchronization, deadlock freedom, multithreaded programs, counter abstraction, predicate abstraction, constrained monotonic abstraction
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-111739 (URN)
Available from: 2014-10-30 Created: 2014-10-30 Last updated: 2014-10-31Bibliographically approved
Ganty, P. & Rezine, A. (2014). Ordered Counter-Abstraction Refinable Subword Relations for Parameterized Verification. In: LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS (LATA 2014): . Paper presented at 8th International Conference on Language and Automata Theory and Applications (LATA) (pp. 396-408). Springer Berlin/Heidelberg, 8370
Open this publication in new window or tab >>Ordered Counter-Abstraction Refinable Subword Relations for Parameterized Verification
2014 (English)In: LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS (LATA 2014), Springer Berlin/Heidelberg, 2014, Vol. 8370, p. 396-408Conference paper, Published paper (Refereed)
Abstract [en]

We present an original refinable subword based symbolic representation for the verification of linearly ordered parameterized systems. Such a system consists of arbitrary many finite processes placed in an array. Processes communicate using global transitions constrained by their relative positions (i.e., priorities). The model can include binary communication, broadcast, shared variables or dynamic creation and deletion of processes. Configurations are finite words of arbitrary lengths. The successful monotonic abstraction approach uses the subword relation to define upward closed sets as symbolic representations for such systems. Natural and automatic refinements remained missing for such symbolic representations. For instance, subword based relations are simply too coarse for automatic forward verification of systems involving priorities. We remedy to this situation and introduce a symbolic representation based on an original combination of counter abstraction with subword based relations. This allows us to define an infinite family of relaxation operators that guarantee termination by a new well quasi ordering argument. The proposed automatic analysis is at least as precise and efficient as monotonic abstraction when performed backwards. It can also be successfully used in forward, something monotonic abstraction is incapable of. We implemented a prototype to illustrate the approach.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2014
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 8370
Keywords
counter abstraction; well quasi ordering; reachability; parameterized verification
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:liu:diva-117675 (URN)10.1007/978-3-319-04921-2_32 (DOI)000352688800032 ()2-s2.0-84898069230 (Scopus ID)978-3-319-04921-2 (ISBN)978-3-319-04920-5 (ISBN)
Conference
8th International Conference on Language and Automata Theory and Applications (LATA)
Available from: 2015-05-11 Created: 2015-05-06 Last updated: 2018-01-31
Abdulla, P. A., Atig, M. F., Chen, Y.-F., Holik, L., Rezine, A., Rümmer, P. & Stenman, J. (2014). String Constraints for Verification. In: 26th International Conference on Computer Aided Verification (CAV 2014), Vienna, Austria, Jul. 9-12, 2014.: . Paper presented at CAV 2014 (pp. 150-166). Berlin: Springer
Open this publication in new window or tab >>String Constraints for Verification
Show others...
2014 (English)In: 26th International Conference on Computer Aided Verification (CAV 2014), Vienna, Austria, Jul. 9-12, 2014., Berlin: Springer, 2014, p. 150-166Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Berlin: Springer, 2014
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 8559
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:liu:diva-114404 (URN)10.1007/978-3-319-08867-9_10 (DOI)978-3-319-08866-2 (ISBN)978-3-319-08867-9 (ISBN)
Conference
CAV 2014
Available from: 2015-02-20 Created: 2015-02-20 Last updated: 2018-02-02
Abdulla, P. A., Haziza, F., Holik, L., Jonsson, B. & Rezine, A. (2013). An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In: Piterman, Nir, Smolka, Scott (Ed.), The 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Rome, Italy, March 16-24, 2013.: . Paper presented at TACAS'13.
Open this publication in new window or tab >>An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
Show others...
2013 (English)In: The 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Rome, Italy, March 16-24, 2013. / [ed] Piterman, Nir, Smolka, Scott, 2013Conference paper, Published paper (Refereed)
Abstract [en]

We present a technique for automatically verifying safety properties of concurrent programs, in particular programs which 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.

Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-92595 (URN)10.1007/978-3-642-36742-7_23 (DOI)000435018600024 ()978-3-642-36742-7 (ISBN)
Conference
TACAS'13
Available from: 2013-05-14 Created: 2013-05-14 Last updated: 2019-07-03
Abdulla, P. A., Atig, M. F., Chen, Y.-F., Leonardsson, C. & Rezine, A. (2013). Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO. In: Tools and Algorithms for the Construction and Analysis of Systems: 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Paper presented at The 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Rome, Italy, March 16-24, 2013. (pp. 530-536). Springer Berlin/Heidelberg
Open this publication in new window or tab >>Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO
Show others...
2013 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Springer Berlin/Heidelberg, 2013, p. 530-536Conference paper, Published paper (Refereed)
Abstract [en]

We introduce MEMORAX, a tool for the verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range and integer variables and running on top of weak memory models. The verification task is non-trivial as it involves exploring state spaces of arbitrary or even infinite sizes. Even for programs that only manipulate finite range variables, the sizes of the store buffers could grow unboundedly, and hence the state spaces that need to be explored could be of infinite size. In addition, MEMORAX in- corporates an interpolation based CEGAR loop to make possible the verification of control state reachability for concurrent programs involving integer variables. The reachability procedure is used to automatically compute possible memory fence placements that guarantee the unreachability of bad control states under TSO. In fact, for programs only involving finite range variables and running on TSO, the fence insertion functionality is complete, i.e., it will find all minimal sets of memory fence placements (minimal in the sense that removing any fence would result in the reachability of the bad control states). This makes MEMORAX the first freely available, open source, push-button verification and fence insertion tool for programs running under TSO with integer variables.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2013
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 7795
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-92596 (URN)10.1007/978-3-642-36742-7_37 (DOI)000435018600038 ()978-3-642-36741-0 (ISBN)978-3-642-36742-7 (ISBN)
Conference
The 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Rome, Italy, March 16-24, 2013.
Available from: 2013-05-14 Created: 2013-05-14 Last updated: 2019-07-03
Organisations

Search in DiVA

Show all publications