- Concurrency
Verification:
Introduction to Compositonal and Noncompositional Methods
.
Willem-Paul de Roever, Frank de Boer,
Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job
Zwiers.Cambridge University Press, 2001. Publisher
information
for this book: UK
site , US
site - Verification of Parameterized Protocols. K. Baukus, Y. Lakhnech and K. Stahl. Journal of Universal Computer Science, vol. 7, no. 2 (2001).
- Incremental Verification by Abstraction. Y. Lakhnech, S. Bensalem, S. Berezin and S. Owre. A conference version of this paper appeared in the proceedings of the 7th International Conference, TACAS 2001, LNCS 20031 Springer-Verlag.
- Iterating Transducers. D. Dams, Y. Lakhnech and M. Steffen. Iterating Transducers. Accepted in CAV'01.
- Analyzing Fair Parametric Extended Automata . A. Annichini, A. Bouajjani, Y. Lakhnech and M. Sighireanu.Accepted at SAS'01
- Networks of Processes with Parameterized State Space. K. Baukus, Y. Lakhnech, S. Bensalem, and K. Stahl. Satellite Workshops, ICALP 2001, ENTCS, pp. 388-402, Crete, Greece, 2001.
- Verifying Untimed and Timed Aspects of the Experimental Batch Plant. Ralf Huuck, Ben Lukoschus and Yassine Lakhnech. European Journal of Control, 7(4):400-415, September 2001. Hermes Science Publishing. ISSN 0947-3580.
2000
- Abstracting WS1S Systems to Verify Prameterized Networks. K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl. A conference version of this paper appeared in the proceedings of the 6th International Conference, TACAS 2000, LNCS 1785, Springer-Verlag.
- Verifying Universal Properties of Parameterized Networks. K. Baukus, Y. Lakhnech, and K. Stahl. Proceedings of FTRTFT 2000.
- A Transformational Approach for Generating Non-linear Invariants. S. Bensalem, M. Bozga, J.-C. Fernandez, L. Ghirvu and Y. Lakhnech. A conference version of this paper appeared in the proceedings of the 7th International Conference, SAS 2000, LNCS 1824, Springer-Verlag.
- Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. P.A. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, P. Habermehl and Y. Lakhnech. A conference version of this paper appeared in theproceedings of CAV'99 LNCS 1633, Springer-Verlag. Copyright of the conference version is held by Springer.© Springer-Verlag.
- Automatic Generation of Invariants. S. Bensalem and Y. Lakhnech. In Formal Methods and System Design 15(1) pp 75-92 July 1999.
- Divide, abstract and model-check. K. Baukus, Y. Lakhnech, K. Stahl, and M. Steffen. A conference version of this paper appeared in the
-
LNCS 1680, Springer-Verlag, 1999.
- Computing Abstractions of Infinite State Systems Compositionally and Automatically(in pdf) . S. Bensalem, Y Lakhnech and S. Owre. A conference version of this paper appears in the proceedings of CAV'98 which will be published as an LNCS, Springer-Verlag. Copyright of the conference version is held by Springer.© Springer-Verlag.
- InVeSt : A Tool for the Verification of Invariants (in pdf) . S. Bensalem, Y Lakhnech and S. Owre. A conference version of this paper appears in the proceedings of CAV'98 which is published as an LNCS, Springer-Verlag. Copyright of the conference version is held by Springer.© Springer-Verlag. 1995
- Synthesizing Different Development Paradigms: Combining Top-Down with Botton-Up Reasoning About Distributed Systems. . J. Zwiers, U. Hannemann, Y. Lakhnech, and W.-P. de Roever. Published in: Foundations of Software Technology and
Theoretical Computer Science.Lecture Notes in Computer Science 1026, 1995.
- Temporal Logic for Stabilizing Systems. . Y. Lakhnech and M. Siegel. Published in: International Conference on Temporal Logic, ICTL 1997.1996
- Modular Completeness: Integrating the Reuse of Specified Software in Top-Down Program Development. J. Zwiers, U. Hannemann, Y. Lakhnech, F. Stomp, and W.-P. de Roever. Published in: Formal Methods Europe, FME'96 Symposium.
Lecture Notes in Computer Science 1051, 1996.
- Powerful Techniques for the Automatic Generation of Invariants. . S. Bensalem, Y. Lakhnech, and H. Saidi. Published in: In Computer Aided Verification, CAV'96. Lecture Notes in Computer Science 1102, 1996.
Go to the top
2000
- Utilizing Static Analysis for Programmable Logic Controllers. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus. ADPM 2000 - The 4th International Conference Automation of Mixed Processes: Hybrid Dynamic Systems.
- An Abstract Model For Sequential Function Charts. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus. WODES 2000 special session ``Formal Models of PLCs''.
- Verification of Sequential Function Charts using SMV. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus. PDPTA 2000 special session on Formal Validation.
- Approaches to the Formal Verification of Hybrid Systems. S. Kowalewski, P. Herrmann, S. Engell, H. Krumm, H. Treseler, Y. Lakhnech, R. , B. Lukoschus. Special issue of ``at-Automatisierungstechnik'' on the DFG research program KONDISK.
-
Integrating
Timed Condition/Event Systems and Timed Automata to the Verificatiion
of
Hybrid Systems. Journal
of Parallel and Distributed Computing Practices 1998.
- Comparing Timed Condition/Event Systems and Timed Automata. Proc. of HART'97, Grenoble, LNCS 1201:81-86, Springer-Verlag, 1997.
- Combining a Computer Science and Control Theory Approach for the Verification of Hybrid Systems. Proc. of the WPDRTS'97, Vienna, 1997.
- Analyse zeitbewerteter Bedingung/Ereignis-Systeme mittels Echtzeitautomaten-Tools. Proc. of the EKA'97, Braunschweig, 1997.
- Using Model-Checking for Timed Automata to Parameterize Logic Control Programs.8th European Symposium on Computer Aided Engineering, Brugge, Belgium, 1997.
- Ahmed Bouajjani, Yassine Lakhnech and Sergio Yovine.Model Checking for Extended Timed Temporal Logics . FTRTFT'96. Lecture Notes in Computer Science 1135, 1996.
- Yassine Lakhnech and Jozef Hooman. Metric Temporal Logic with Durations . Published in:Theoretical Computer Science 138, 1995.
- Ahmed Bouajjani, Yassine Lakhnech, and Riadh Robbana.From Duration Calculus to Hybrid Automata . Published in: Proceedings of the 7th Int. Conf. on Computer Aided Verification, Lecture Notes in Computer Science 939, pp. 196--210, 1995.
- Ahmed Bouajjani and Yassine Lakhnech. Logics vs. Automata: The Hybrid Case . Published in: Hybrid Systems Workshop DIMACS'95, Lecture Notes in Computer Science 1066, 1995.
Ahmed Bouajjani and Yassine Lakhnech. Timed Automata + Temporal Logic: Expressiveness and Decidability . Published in: Proceedings of the 6th CONCUR'95: Concurrency Theory, Lecture Notes in Computer Science 962, pp. 531--546, 1995.
- Yassine Lakhnech and Jozef Hooman. Reasoning about durations in metric temporal logic . Published in: Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, pp. 488--510, 1994.
Go to the top
- E. Mikk, Y. Lakhnech, C. Petersohn, and M. Siegel. On formal semantics of Statecharts as supported by STATEMATE . In 2nd BCS-FACS Northern Formal Methods Workshop. Springer-Verlag, July 97.
- E. Mikk, Y. Lakhnech, and M. Siegel.Hierarchical automata as model for statecharts.In Asian Computing Science Conference (ASIAN'97), volume 1345 of LNCS. Springer Verlag, December 97.
- E. Mikk, Y. Lakhnech, M. Siegel,
and
G. J.
Holzmann. Implementing
Statecharts in Promela/SPIN. In proceedings of WIFT98.