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

Direct link
BETA
Rezine, Ahmed
Publications (10 of 12) Show all publications
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: Piterman, Nir; Smolka, ScottA. (Ed.), Tools and Algorithms for the Construction and Analysis of Systems: . Paper presented at 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, March 16-24, 2013, Rome, Italy (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, Springer Berlin/Heidelberg, 2013, p. 530-536Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2013
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7795
National Category
Software Engineering
Identifiers
urn:nbn:se:uu:diva-203169 (URN)10.1007/978-3-642-36742-7_37 (DOI)978-3-642-36741-0 (ISBN)
Conference
19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, March 16-24, 2013, Rome, Italy
Projects
UPMARCWeak Memory Models
Available from: 2013-07-03 Created: 2013-07-03 Last updated: 2018-01-11Bibliographically approved
Abdulla, P. A., Chen, Y.-F., Delzanno, G., Haziza, F., Hong, C.-D. & Rezine, A. (2010). Constrained monotonic abstraction: A CEGAR for parameterized verification. In: CONCUR 2010 – Concurrency Theory. Paper presented at 21st International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010 (pp. 86-101). Berlin: Springer-Verlag
Open this publication in new window or tab >>Constrained monotonic abstraction: A CEGAR for parameterized verification
Show others...
2010 (English)In: CONCUR 2010 – Concurrency Theory, Berlin: Springer-Verlag , 2010, p. 86-101Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we develop a counterexample-guided abstraction refinement (CEGAR) framework for monotonic abstraction, an approach that is particularly useful in automatic verification of safety properties for parameterized systems The main drawback of verification using monotonic abstraction is that it sometimes generates spurious counterexamples Our CEGAR algorithm automatically extracts from each spurious counterexample a set of configurations called a "Safety Zone" and uses it to refine the abstract transition system of the next iteration We have developed a prototype based on this idea, and our experimentation shows that the approach allows to verify many of the examples that cannot be handled by the original monotonic abstraction approach.

Place, publisher, year, edition, pages
Berlin: Springer-Verlag, 2010
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6269
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-130923 (URN)10.1007/978-3-642-15375-4_7 (DOI)000285373500007 ()978-3-642-15374-7 (ISBN)
Conference
21st International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010
Projects
UPMARCautomated verification of highly concurrent algorithms
Available from: 2010-09-17 Created: 2010-09-17 Last updated: 2018-01-12Bibliographically approved
Bouajjani, A., Dragoi, C., Enea, C., Rezine, A. & Sighireanu, M. (2010). Invariant synthesis for programs manipulating lists with unbounded data. In: Computer Aided Verification (pp. 72-88). Berlin: Springer-Verlag
Open this publication in new window or tab >>Invariant synthesis for programs manipulating lists with unbounded data
Show others...
2010 (English)In: Computer Aided Verification, Berlin: Springer-Verlag , 2010, p. 72-88Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Berlin: Springer-Verlag, 2010
Series
Lecture Notes in Computer Science ; 6174
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-130921 (URN)10.1007/978-3-642-14295-6_8 (DOI)978-3-642-14294-9 (ISBN)
Available from: 2010-09-17 Created: 2010-09-17 Last updated: 2018-01-12Bibliographically approved
Abdulla, A., Delzanno, G. & Rezine, A. (2009). Approximated Context-Sensitive Analysis for Parameterized Verification. In: David Lee, Antónia Lopes and Arnd Poetzsch-Heffter (Ed.), Formal Techniques for Distributed Systems: Joint 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009, Lisboa, Portugal, June 9-12, 2009. Proceedings (pp. 41-56). , 5522
Open this publication in new window or tab >>Approximated Context-Sensitive Analysis for Parameterized Verification
2009 (English)In: Formal Techniques for Distributed Systems: Joint 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009, Lisboa, Portugal, June 9-12, 2009. Proceedings / [ed] David Lee, Antónia Lopes and Arnd Poetzsch-Heffter, 2009, Vol. 5522, p. 41-56Conference paper, Published paper (Other academic)
Series
Lecture notes in computer science, ISSN 0302-9743 ; 5522
National Category
Engineering and Technology
Identifiers
urn:nbn:se:uu:diva-130925 (URN)10.1007/978-3-642-02138-1_3 (DOI)978-3-642-02137-4 (ISBN)
Available from: 2010-09-17 Created: 2010-09-17 Last updated: 2010-09-27Bibliographically approved
Abdulla, A., Delzanno, G. & Rezine, A. (2009). Approximated parameterized verification of infinite-state processes with global conditions. Formal methods in system design, 34(2), 126-156
Open this publication in new window or tab >>Approximated parameterized verification of infinite-state processes with global conditions
2009 (English)In: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 34, no 2, p. 126-156Article in journal (Refereed) Published
National Category
Engineering and Technology
Identifiers
urn:nbn:se:uu:diva-130929 (URN)10.1007/s10703-008-0062-9 (DOI)000263683200003 ()
Available from: 2010-09-17 Created: 2010-09-17 Last updated: 2017-12-12Bibliographically approved
Abdulla, A., Delzanno, G. & Rezine, A. (2009). Automatic Verification of Directory-Based Consistency Protocols. In: Olivier Bournez and Igor Potapov (Ed.), Reachability Problems: 3rd International Workshop, RP 2009, Palaiseau, France, September 23-25, 2009. Proceedings (pp. 36-50). , 5797
Open this publication in new window or tab >>Automatic Verification of Directory-Based Consistency Protocols
2009 (English)In: Reachability Problems: 3rd International Workshop, RP 2009, Palaiseau, France, September 23-25, 2009. Proceedings / [ed] Olivier Bournez and Igor Potapov, 2009, Vol. 5797, p. 36-50Conference paper, Published paper (Other academic)
Series
Lecture notes in computer science, ISSN 0302-9743 ; 5797
National Category
Engineering and Technology
Identifiers
urn:nbn:se:uu:diva-130927 (URN)10.1007/978-3-642-04420-5_6 (DOI)978-3-642-04419-9 (ISBN)
Available from: 2010-09-17 Created: 2010-09-17 Last updated: 2010-09-27Bibliographically approved
Abdulla, A., Delzanno, G., Henda, B. & Rezine, A. (2009). Monotonic Abstraction: on Efficient Verification of Parameterized Systems. International Journal of Foundations of Computer Science, 20(5), 779-801
Open this publication in new window or tab >>Monotonic Abstraction: on Efficient Verification of Parameterized Systems
2009 (English)In: International Journal of Foundations of Computer Science, ISSN 0129-0541, Vol. 20, no 5, p. 779-801Article in journal (Refereed) Published
Abstract [en]

We introduce the simple and efficient method of monotonic abstraction to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables over finite domains. The method of monotonic abstraction derives an over-approximation of the induced transition system that allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype that works well on several mutual exclusion algorithms and cache coherence protocols

National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-130930 (URN)10.1142/S0129054109006887 (DOI)000272248900002 ()
Projects
apvUPMARCautomated verification of highly concurrent algorithms
Available from: 2010-09-17 Created: 2010-09-17 Last updated: 2018-01-12Bibliographically approved
Abdulla, A., Delzanno, G. & Rezine, A. (2008). Monotonic Abstraction in Parameterized Verification. Electronical Notes in Theoretical Computer Science, 223, 3-14
Open this publication in new window or tab >>Monotonic Abstraction in Parameterized Verification
2008 (English)In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 223, p. 3-14Article in journal (Refereed) Published
National Category
Engineering and Technology
Identifiers
urn:nbn:se:uu:diva-130931 (URN)10.1016/j.entcs.2008.12.027 (DOI)
Available from: 2010-09-17 Created: 2010-09-17 Last updated: 2017-12-12Bibliographically approved
Rezine, A. (2008). Parameterized Systems: Generalizing and Simplifying Automatic Verification. (Doctoral dissertation). Uppsala: Acta Universitatis Upsaliensis
Open this publication in new window or tab >>Parameterized Systems: Generalizing and Simplifying Automatic Verification
2008 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

In this thesis we propose general and simple methods for automatic verification of parameterized systems. These are systems consisting of an arbitrary number of identical processes or components. The number of processes defines the size of the system. A parameterized system may be regarded as an infinite family of instances, namely one for each size. The aim is to perform a parameterized verification, i.e. to verify that behaviors produced by all instances, regardless of their size, comply with some safety or liveness property. In this work, we describe three approaches to parameterized verification.

First, we extend the Regular Model Checking framework to systems where components are organized in tree-like structures. For such systems, we give a methodology for computing the set of reachable configurations (used to verify safety properties) and the transitive closure (used to verify liveness properties).

Next, we introduce a methodology allowing the verification of safety properties for a large class of parameterized systems. We focus on systems where components are organized in linear arrays and manipulate variables or arrays of variables ranging over bounded or numerical domains. We perform backwards reachability analysis on a uniform over-approximation of the parameterized system at hand.

Finally, we suggest a new approach that enables us to reduce the verification of termination under weak fairness conditions to a reachability analysis for systems with simple commutativity properties. The idea is that reachability calculations (associated with safety) are usually less expensive then termination (associated with liveness). This idea can also be used for other transition systems and not only those induced by parameterized systems.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2008. p. 196
Series
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 72
Keywords
Parameterized systems, Automatic verification, Approximation, Regular model checking, Safety, Termination
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-8587 (URN)978-91-554-7138-5 (ISBN)
Public defence
2008-04-15, Room 2446, Polacksbacken, Lägerhyddsvägen 2D, Uppsala, 10:00 (English)
Opponent
Supervisors
Available from: 2008-03-27 Created: 2008-03-27 Last updated: 2018-01-13Bibliographically approved
Abdulla, P., Delzanno, G. & Rezine, A. (2007). Parameterized Verification of Infinite-state Processes with Global Conditions. In: Damm W, Hermanns H (Ed.), Computer Aided Verification, Proceedings. Paper presented at 19th International Conference on Computer Aided Verification Berlin, GERMANY, JUL 03-07, 2007 (pp. 145-157).
Open this publication in new window or tab >>Parameterized Verification of Infinite-state Processes with Global Conditions
2007 (English)In: Computer Aided Verification, Proceedings / [ed] Damm W, Hermanns H, 2007, p. 145-157Conference paper, Published paper (Refereed)
Abstract [en]

We present a simple and effective approximated backward reachability algorithm for parameterized systems with existentially and universally quantified global conditions. The individual processes operate on unbounded local variables ranging over the natural numbers. In addition, processes may communicate via broadcast, rendez-vous and shared variables. We apply the algorithm to verify mutual exclusion for complex protocols such as Lamport's bakery algorithm both with and without atomicity conditions, a distributed version of the bakery algorithm, and Ricart-Agrawala's distributed mutual exclusion algorithm.

Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 4590
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:uu:diva-10733 (URN)000248222700014 ()978-3-540-73367-6 (ISBN)
Conference
19th International Conference on Computer Aided Verification Berlin, GERMANY, JUL 03-07, 2007
Available from: 2007-06-25 Created: 2007-06-25 Last updated: 2018-01-12Bibliographically approved
Organisations

Search in DiVA

Show all publications