List of publications

A. Bouajjani, C. Enea, J. Hamza,
Verifying Eventual Consistency of Optimistic Replication Systems,
In Proc. 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL'14), San Diego (Ca, USA), January 2014.

A. Bouajjani, M. Emmi, C. Enea, J. Hamza,
Verifying Concurrent Programs against Sequential Specifications,
In Proc. 22nd European Symposium on Programming (ESOP'13), Rome (Italy), March 2013.

A. Bouajjani, E. Derevenetc, R. Meyer,
Checking and Enforcing Robustness against TSO,
In Proc. 22nd European Symposium on Programming (ESOP'13), Rome (Italy), March 2013.

A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu,
Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data,
In Proc. 10th Intern. Symp. on Automated Technology for Verification and Analysis (ATVA'12), Thiruvananthapuram (India), October 2012.

M. F. Atig, A. Bouajjani, K. Narayan Kumar, P. Saivasan,
LinearTime ModelChecking for Multithreaded Programs under ScopeBounding,
In Proc. 10th Intern. Symp. on Automated Technology for Verification and Analysis (ATVA'12), Thiruvananthapuram (India), October 2012.

M. F. Atig, A. Bouajjani, M. Emmi, A. Lal,
Detecting Fair NonTermination in Multithreaded Programs,
In Proc. 24th International Conference on Computer Aided Verification (CAV'12), Berkeley (Ca, USA), July 2012.

M. F. Atig, A. Bouajjani, S. Burckhardt, M. Musuvathi,
What's Decidable about Weak Memory Models?,
In Proc. 21st European Symposium on Programming (ESOP'12), Tallinn (Estonia), March 2012.

A. Bouajjani, M. Emmi,
Bounded Phase Analysis of MessagePassing Programs,
In Proc. 18th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), Tallinn (Estonia), March 2012.

A. Bouajjani, M. Emmi,
Analysis of Recursively Parallel Programs,
In Proc. 39th ACM Symposium on Principles of Programming Languages (POPL'12), Philadelphia (Penn, USA), January 2012.

A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu,
Abstract Domains for Automated Reasoning about ListManipulating Programs with Infinite Data, Invited paper,
In Proc. 13th Intern. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'12), Philadelphia (Penn, USA), January 2012.

A. Bouajjani, M. Emmi, G. Parlato,
On Sequentializing Concurrrent Programs,
In Proc. 18th International Static Analysis Symposium (SAS'11), LNCS 6887, Venice (Italy), September 2011.

A. Bouajjani, R. Meyer, E. Moehlmann,
Deciding Robustness Against Total Store Ordering,
In Proc. 38th International Colloquium on Automata, Languages and Programming (ICALP'11), LNCS 6756, Zurich (Switzerland), July 2011.

M. F. Atig, A. Bouajjani, G. Parlato,
Getting Rid of StoreBuffers in the Analysis of Weak Memory Models,
In Proc. 23nd Intern. Conf. on Computer Aided Verification (CAV'11), LNCS 6806, Snowbird, Utah (USA), July 2011.

A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu,
On InterProcedural Analysis of Programs with Lists and Data ,
In Proc. 32nd ACM Conference on Programming Language Design and Implementation (PLDI'11), San Jose, (Ca, USA), June 2011.

A. Bouajjani, C. Dragoi, C. Enea, A. Rezine, M. Sighireanu,
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data,
In Proc. 22nd Intern. Conf. on Computer Aided Verification (CAV'10), to appear in LNCS, Edinburgh (UK), July 2010.

M. F. Atig, A. Bouajjani, S. Burckhardt, M. Musuvathi,
On the Verification Problem for Weak Memory Models,
In Proc. 37th ACM Symp. on Principles of Programming Languages (POPL'10), Madrid (Spain), January 2010.

A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu,
A Logicbased Framework for Reasoning about Composite Data Structures,
In Proc. 20th Intern. Conf. on Concurrency Theory (CONCUR'09),
LNCS 5710, Bologna (Italy), September 2009.

M. F. Atig, A. Bouajjani, S. Qadeer,
Contextbounded analysis for concurrent programs with dynamic creation of threads,
In Proc. 15th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09),
LNCS 5505, York (UK), March 2009.

M. F. Atig, A. Bouajjani, T. Touili,
Analyzing Asynchronous Programs with Preemption,
In Proc. 28th Intern. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'08),
Bangalore (India), December 2008.

M. F. Atig, A. Bouajjani, T. Touili,
On the Reachability Analysis of Acyclic Networks of Pushdown Systems,
In Proc. 19th Intern. Conf. on Concurrency Theory (CONCUR'08),
LNCS 5201, Toronto (Canada), August 2008.

P. A. Abdulla, A. Bouajjani, L. Holik, L. Kaati, T. Vojnar ,
Composed Bisimulations over Tree Automata,
In Proc. 13th Intern. Conference on Implementation and Application of Automata (CIAA'08),
LNCS 5148, San Francisco (USA), July 2008.

A. Bouajjani, P. Habermehl, L. Holik, T. Touili, T. Vojnar ,
Antichainbased Universality and Inculsion Testing over Nondeterministic Finite Tree Automata,
In Proc. 13th Intern. Conference on Implementation and Application of Automata (CIAA'08),
LNCS 5148, San Francisco (USA), July 2008.

P. A. Abdulla, A. Bouajjani, J. Cederberg, F. Haziza, A. Rezine ,
Monotonic Abstraction for Programs with Dynamic Memory Heaps,
In Proc. 20th Intern. Conf. on Computer Aided Verification (CAV'08),
LNCS 5123, Princeton (USA), July 2008.

P. A. Abdulla, A. Bouajjani, L. Holik, L. Kaati, T. Vojnar ,
Computing Simulations over Tree Automata (Efficient Techniques for Reducing Tree Automata) ,
In Proc. 14th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08),
LNCS 4963, Budapest (Hungary), April 2008.

A. Bouajjani, J. Esparza, S. Schwoon, D. Suwimonteerabuth ,
SDSIrep: A Reputation System based on SDSI ,
In Proc. 14th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08),
LNCS 4963, Budapest (Hungary), April 2008.

A. Bouajjani, P. Habermehl, Y. Jurski, M. Sighireanu,
Rewriting Systems with Data: A Framework for Reasoning about Systems with Unbounded Structures over Infinite Data Domains,
Invited paper,
In Proc. 16th Intern. Symp. on Fundamentals of Computation Theory (FCT'07).
LNCS 4639, Budapest (Hungary), August 2007. ( pdf file ).

A. Bouajjani, S. Fratani, S. Qadeer,
ContextBounded Analysis of Multithreaded Programs with Dynamic Linked Structures,
In Proc. Intern. Conf. on Computer Aided Verification
(CAV'07) ,
LNCS 4590, Berlin (Germany), July 2007.
( pdf file ).

A. Bouajjani, Y. Jurski, M. Sighireanu,
A Generic Framework for Reasoning about Dynamic Networks of InfiniteState Processes,
In Proc. 13th Intern. Conf. on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS'07)
LNCS 4424, Braga (Portugal), March 2007. ( pdf file ). Full version
( pdf file ).

A. Bouajjani, P. Habermehl, A. Rogalewicz, T. Vojnar ,
Abstract Tree Regular Model Checking of Complex Dynamic Data Structures ,
In Proc. Intern. Static Analysis Symposium
(SAS'06) ,
LNCS 4218, Seoul (Korea), August 2006.
( pdf file )

A. Bouajjani, J. Strejcek, T. Touili,
On Symbolic Verification of Weakly Extended PAD,
In Proc. Intern. Workshop on Expressiveness in Concurrency
(EXPRESS'06) ,
August 2006. Published in ENTCS 175(3), 2007.

A. Bouajjani, J. Esparza ,
Rewriting Models of Boolean Programs ,
In Proc. Intern. Conf. on Rewriting Techniques and Applications
(RTA'06) , invited paper,
LNCS 4098, Seattle (USA), August 2006.
( pdf file )

A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, T. Vojnar ,
Programs with Lists are Counter Automata ,
In Proc. Intern. Conf. on Computer Aided Verification
(CAV'06) ,
LNCS 4144, Seattle (USA), August 2006
( pdf file ). Long version: ( pdf file ).

G. Yorsh, A. Rabinovich, M. Sagiv, A. Meyer, A. Bouajjani,
A Logic of Reachable Patterns in Linked DataStructures,
In Proc. Intern. Conf. on Foundations of Software Science and Computer Structure (FOSSACS'06),
LNCS 3921, Vienna (Austria), March 2006.
( gziped postscript )

A. Bouajjani, J. Esparza, S. Schwoon, J. Strejcek,
Reachability Analysis of Multithreaded Software with Asynchronous Communication,
In Proc. 25th Intern. Conf. on Foundations of Software Technology and
Theoretical Computer Science
(FSTTCS'05) ,
LNCS 3821, Hyderabad (India), December 2005.
( gziped postscript )

A. Bouajjani, M. MuellerOlm, T. Touili,
Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems,
In Proc. 16th Intern. Conf. on Concurrency Theory (CONCUR'05),
LNCS 3653, San Francisco (Ca, USA), August 2005.
( pdf file )
Long version available at
( gziped postscript )

A. Bouajjani, T. Touili,
On Computing Reachability Sets of Process Rewrite Systems ,
In Proc. 16th Intern. Conf. on Rewriting Techniques
and Applications (RTA'05),
LNCS 3467, Nara (Japan), April 2005.
( gziped PostScript )

A. Bouajjani, P. Habermehl, P. Moro, T. Vojnar,
Verifying Programs with Dynamic 1SelectorLinked Structures in
Regular Model Checking ,
In Proc. 11th Intern. Conf. on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS'05)
LNCS 3440, Edinburgh (UK), April 2005.
( gziped PostScript )

A. Bouajjani, A. Meyer ,
Symbolic Reachability Analysis of HigherOrder
ContextFree Processes
In Proc. 24th Intern. Conf. on Foundations of Software Technology and
Theoretical Computer Science
(FSTTCS'04) ,
LNCS 3328, Madras (India), December 2004.
( gziped PostScript )

A. Bouajjani, A. Legay, P. Wolper,
Handling Liveness Properties in (omega)Regular
Model Checking,
In Proc. 6th Intern. Workshop on Verification of InfiniteState Systems
(Infinity'04), London (UK), September 2004. to appear in ENTCS.
( gziped PDF )

A. Bouajjani, J. Esparza, T. Touili,
Reachability Analysis of Synchronized PA Systems,
In Proc. 6th Intern. Workshop on Verification of InfiniteState Systems
(Infinity'04), London (UK), September 2004. to appear in ENTCS.
( gziped PostScript )

A. Bouajjani, P. Habermehl, T. Vojnar,
Abstract Regular Model Checking ,
In Proc. 16th Intern. Conf. on Computer Aided Verification
(CAV'04),
LNCS 3114, Boston (Ma, USA), July 2004.
( gziped PostScript )

P. A. Abdulla, A. CollombAnnichini, A. Bouajjani,
B. Jonsson,
Using Forward Reachability Analysis for Verification of Lossy Channel Systems ,
In Formal Methods in System Design, volume 25, no 1, pp 3965,
Kluwer Academic Pub., July 2004.
( gziped PostScript )

A. Bouajjani, T. Touili ,
Reachability Analysis of Process Rewrite Systems
,
in Proc. 23rd Intern. Conf. on Foundations of Software Technology and
Theoretical Computer Science
(FSTTCS'03) ,
LNCS 2914, Mumbai (India), December 2003.
( gziped PostScript )

A. Bouajjani, P. Habermehl, T. Vojnar ,
Verification of Parametric Concurrent Systems with
Prioritized FIFO Resource Management
,
in Proc. Intern. Conf. on Concurrency Theory
(CONCUR'03) ,
LNCS 2761, Marseille (France), September 2003.
( gziped PostScript )

P. A. Abdulla, A. Bouajjani, J. d'Orso ,
Deciding Monotonic Games
,
in Proc. Intern. Workshop Computer Science Logic
(CSL'03) ,
LNCS 2803, Vienna (Austria), August 2003.
( gziped PostScript )

A. Bouajjani, J. Esparza, T. Touili ,
A Generic Approach to the Static Analysis
of Concurrent Programs with Procedures
,
in Proc. 30th Intern. ACM Symp. on Principles of Programming Languages
(POPL'03) ,
New Orleans (Louisiana, USA), January 2003.
( gziped PostScript ).
Full version in the International Journal of Foundations of Computer Science
, volume 14, no 4, August 2003.
( gziped PostScript ).

A. Bouajjani, A. Merceron ,
Parametric Verification of a Group Membership
Algorithm ,
in Proc. 7th Intern. Symp. on Formal Techniques in RealTime and
Fault Tolerant Systems
(FTRTFT'02) ,
LNCS 2469, Oldenburg (Germany), September 2002.
( gziped PostScript )

A. Bouajjani, T. Touili ,
Extrapolating Tree Transformations ,
in Proc. 14th Intern. Conf. on Computer Aided Verification
(CAV'02) ,
LNCS 2404, Copenhagen (Denmark), July 2002.
( gziped PostScript )

A. Bouajjani, P. Habermehl, R. Mayr ,
Automatic Verification of Recursive Procedures with one Integer Parameter
,
in Proc. 26th Intern. Symp. on Mathematical Foundations of Computer Science
(MFCS'01) ,
LNCS 2136, Marianske Lazne (Czech Republic), August 2001.
( gziped PostScript ).
Full version in the journal Theoretical Computer Science , volume 295, 2003.
( gziped PostScript ).
Presentation available ( PDF ).

A. Annichini, A. Bouajjani, M. Sighireanu ,
TReX: A Tool for Reachability Analysis of Complex Systems ,
in Proc. 13th Intern. Conf. on Computer Aided Verification
(CAV'01) ,
LNCS 2102, Paris (France), July 2001.
( gziped PostScript )

A. Annichini, A. Bouajjani, Y. Lakhnech, M. Sighireanu ,
Analyzing Fair Parametric Extended Automata ,
in Proc. 8th Intern. Static Analysis Symposium
(SAS'01) , LNCS 2126, Paris (France), July 2001.
( gziped PostScript )

A. Bouajjani ,
Languages, Rewriting systems, and Verification of InfiniteState Systems ,invited paper, in Proc. 28th Intern. Coll. on Automata, Languages and Programming
(ICALP'01) ,
LNCS 2076, Crete (Greece), July 2001.
( gziped PostScript )

P. Abdulla, L. Boasson, A. Bouajjani ,
Effective Lossy Queue Languages ,
in Proc. 28th Intern. Coll. on Automata, Languages and
Programming
(ICALP'01) ,
LNCS 2076, Crete (Greece), July 2001.
( gziped PostScript )

E. Asarin, A. Bouajjani ,
Perturbed Machines and Hybrid Systems ,
in
Proc. 16th IEEE Symp. on Logic in Computer Science
(LICS'01) , Boston (Ma, USA), June 2001.
( gziped PostScript )

A. Bouajjani, A. Muscholl, T. Touili ,
Permutation Rewriting and Algorithmic Verification ,
in Proc. 16th IEEE Symp. on Logic in Computer Science
(LICS'01) , Boston (Ma, USA), June 2001.
( gziped PostScript ).
Full version available
( gziped PostScript ).

A. Bouajjani, J. Esparza, A. Finkel, O. Maler, P. Rossmanith, B. Willems, P. Wolper ,
An Efficient Automata Approach to Some Problems on ContextFree Grammars
,
in the journal
Information Processing Letters , volume 74, 2000.
( gziped PostScript )

A. Annichini, E. Asarin, A. Bouajjani ,
Symbolic Techniques for Parametric Reasoning about
Counter and Clock Systems ,
in Proc. 12th Intern. Conf. on Computer Aided Verification
(CAV'00) , LNCS 1855, Chicago (Il, USA), July 2000.
( gziped PostScript )

A. Bouajjani, B. Jonsson, M. Nilsson, T. Touili ,
Regular Model Checking , in
Proc. 12th Intern. Conf. on Computer Aided Verification
(CAV'00) , LNCS 1855, Chicago (Il, USA), July 2000.
( gziped PostScript )

P. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani,
P. Habermehl, Y. Lakhnech ,
Verification of InfiniteState Systems by Combining Abstraction
and Reachability Analysis ,
in Proc. 11th Intern. Conf. on Computer Aided Verification
(CAV'99) , LNCS 1633, Trento (Italy), June 1999.
( gziped PostScript )

P. Abdulla, A. Bouajjani, B. Jonsson, M. Nilsson ,
Handling Global Conditions in Parametrized System Verification ,
in Proc. 11th Intern. Conf. on Computer Aided Verification
(CAV'99) , LNCS 1633, Trento (Italy), June 1999.
( gziped PostScript )

P. Abdulla, A. Annichini, A. Bouajjani ,
Symbolic Verification of Lossy Channel Systems: Application
to the Bounded Retransmission Protocol ,
in Proc. 5th Intern. Conf. on Tools and Algorithms for
the Construction and Analysis of Systems
(TACAS'99) , LNCS 1579,
Amsterdam (Netherland), March 1999.
( gziped PostScript )

A. Bouajjani, R. Mayr ,
Model Checking Lossy Vector Addition Systems ,
in Proc. 16th Intern.
Symp. on Theoretical Aspects in Computer Science
(STACS'99) , LNCS 1563,
Trier (Germany), March 1999.
( gziped PostScript )

P. Abdulla, A. Bouajjani, B. Jonsson ,
OntheFly Analysis of Systems with Unbounded, Lossy Fifo Channels ,
in Proc. 10th Intern. Conf. on Computer Aided Verification
(CAV'98) ,
LNCS 1427, Vancouver (Canada), June 1998.
( gziped PostScript )

A. Bouajjani, S. Tripakis, S. Yovine ,
OntheFly Symbolic ModelChecking of RealTime Systems ,
in Proc. 18th IEEE RealTime Systems Symposiu}
(RTSS'97) , San Francisco (Ca, USA), December 1997.

A. Bouajjani, P. Habermehl ,
Symbolic Reachability Analysis of FifoChannel Systems with
Nonregular Sets of Configurations ,
in Proc. 24th Intern. Coll. on Automata, Languages and
Programming
(ICALP'97) , LNCS 1256, Bologna (Italy), July 1997.
Full version in the journal of
Theoretical Computer Science ,
volume 221, number 1/2, pages 221250, 1999.
( gziped PostScript )

A. Bouajjani, J. Esparza, O. Maler ,
Reachability Analysis of Pushdown Automata: Application to Model Checking
,
in Proc. 8th Intern. Conf. on Concurrency Theory
(CONCUR'97) ,
LNCS 1243, Warsaw (Poland), June 1997.
( gziped PostScript )

A. Bouajjani, O. Maler ,
Reachability Analysis of Pushdown Automata
,
in Proc. Intern. Workshop on Verification of InfiniteState Systems
(Infinity'96) , Pisa (Italy),
Techn. Report MIP9614, Faculty of Mathematics and Computer Science,
University of Passau, 1996.
( gziped PostScript )

A. Bouajjani, Y. Lakhnech, S. Yovine ,
Model Checking for Extended Timed Temporal Logics ,
in Proc. Intern. Symp. on Formal Techniques in Real Time
and Fault Tolerant Systems
(FTRTFT'96) ,
LNCS 1135, Uppsala (Sweden), September 1996.

A. Bouajjani, P. Habermehl ,
Constrained Properties, Semilinear Systems, and Petri Nets ,
in Proc. 7th Intern. Conf. on Concurrency Theory
(CONCUR'96) ,
LNCS 1119, Pisa (Italy), August 1996.
( gziped PostScript )

A. Bouajjani, Y. Lakhnech ,
Logics vs. Automata: The Hybrid Case ,
in Proc. Hybrid System III: Verification and Control , LNCS 1066, 1996.

A. Bouajjani, R. Echahed, R. Robbana ,
On the Automatic Verification of Systems
with Continuous Variables and Unbounded Discrete Data Structures ,
in Proc. Hybrid System II , LNCS 999, 1995.
( gziped PostScript )

A. Bouajjani, Y. Lakhnech ,
Temporal Logic + Timed Automata: Expressiveness and Decidability ,
in Proc. 6th Intern. Conf. on Concurrency Theory
(CONCUR'95) ,
LNCS 962, Philadelphia (Penn, USA), August 1995.
( gziped PostScript )

A. Bouajjani, Y. Lakhnech, R. Robbana ,
From Duration Calculus to Linear Hybrid Automata ,
in Proc. 7th Intern. Conf. on Computer Aided Verification
(CAV'95) ,
LNCS 939, Liege (Belgium), July 1995.

A. Bouajjani, R. Robbana ,
Verifying omegaRegular Properties for a Subclass of Linear Hybrid Systems
,
in Proc. 7th Intern. Conf. on Computer Aided Verification
(CAV'95) ,
LNCS 939, Liege (Belgium), July 1995.

A. Bouajjani, R. Echahed, P. Habermehl ,
On the Verification Problem of Nonregular Properties for Nonregular Processes
,
in Proc. 10th IEEE Symp. on Logic in Computer Science
(LICS'95) ,
San Diego (Ca, USA), June 1995.

A. Bouajjani, R. Echahed, P. Habermehl ,
Verifying Infinite State Processes with Sequential and Parallel Composition
,
in Proc. 22nd ACM Symp. on Principles of Programming Languages
(POPL'95) , San Francisco (Ca, USA), January 1995.

C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem ,
Property Preserving Abstractions for the Verification of Concurrent Systems
, in journal of
Formal Methods in System Design ,
volume 6, pages 1144, 1995.
( gziped PostScript )

A. Bouajjani, R. Echahed, R. Robbana ,
Verifying Invariance Properties of Timed Systems with Duration Variables
, in Proc. Intern. Symp. on Formal Techniques in Real Time and Fault Tolerant Systems
(FTRTFT'94) , LNCS 863, Lübeck (Germany), September 1994.

A. Bouajjani, R. Echahed, R. Robbana ,
Verification of Nonregular Temporal Properties for ContextFree Processes
,
in Proc. 5th Intern. Conf. on Concurrency Theory
(CONCUR'94) ,
LNCS 836, Uppsala (Sweden), August 1994.

A. Bouajjani, R. Echahed, R. Robbana ,
Verification of ContextFree Timed Systems using Linear Hybrid Observers ,in Proc. 6th Intern. Conf. on ComputerAided Verification
(CAV'94) ,
LNCS 818, Stanford (Ca, USA), June 1994.

A. Bouajjani, R. Echahed, J. Sifakis ,
On Model Checking for RealTime Properties with Durations ,
in Proc. 8th IEEE Symp. on Logic in Computer Science
(LICS'93) ,
Montreal (Canada), June 1993.

A. Bouajjani, JC. Fernandez, N. Halbwachs, C. Ratel, P. Raymond ,
Minimal State Graph Generation ,
in the journal
Science of Computer Programming ,
volume 18, pages 247269, 1992.

A. Bouajjani, S. Bensalem, C. Loiseaux, J. Sifakis
Property Preserving Simulations ,
in Proc. 4th Intern. Conf. on ComputerAided Verification
(CAV'92) ,
LNCS 663, Montreal, 1992.

A. Bouajjani, JC. Fernandez, S. Graf, C. Rodriguez, J. Sifakis ,
Safety Properties for BranchingTime Semantics ,
in Proc. 18th Intern. Coll. on Automata, Languages and
Programming
(ICALP'91) ,
LNCS 501, Madrid (Spain), July 1991.

A. Bouajjani, JC. Fernandez, N. Halbwachs ,
Minimal Model Generation ,
in Proc. 2nd Intern. Conf. on ComputerAided Verification
(CAV'90) ,
AMSACM series on Discrete Mathematics and Theoretical Computer Science,
Rutgers (NJ, USA), June 1990.