=. Boolean and . Exists, INT) : 1 <= i AND i <= N AND p[i]

N. Forall, INT) : 1 <= i AND i <= N AND (p1[i]

N. Forall, INT) : 1 <= i AND i <= N AND p[i]

%. Xtgs and %. Init, BOOLEAN = FORALL (i:INT) : 1 <= i AND i <= N AND p[i]

%. %%%-righthand-nodes-prime and . N01_a1, BOOLEAN = (k1 = 0) AND (1 <= i AND i <= N) AND (p1[i]

%. %%%-lefthand-nodes-prime and . Nl11_a1, BOOLEAN = (1 <= i AND i <= N) AND p1[i]

%. Xtgs and %. Init, AND (1 <= i AND i <= N ) AND p[i].loc=0 AND p[i].cs = 0 AND p[i].c=0 AND FORALL (j:INT) : j /= i AND (1 <= j AND j <= N)

A. , A. <=, A. , and <. Forall, INT) : (j /= i AND 1 <= j AND j <= N) => ( p1

A. Nr1_aa, A. <=, <. N. And, /. =. , and A. Exists, INT) : (j /= i AND 1 <= j AND j <= N) AND k1=j => ( FORALL (t:INT) : (t /= j AND 1 <= t AND t <= N) => ( p1

A. N0_aa, A. <=, and <. Exists, INT) : (j /= i AND 1 <= j AND j <= N AND k1=j) => ( FORALL (t:INT) : (t /= j AND 1 <= t AND t <= N) => ( p1

A. , A. <=, A. , and <. Exists, INT) : (j /= i AND 1 <= j AND j <= N) => (FORALL (t:INT) : (t /= j AND 1 <= t AND t <= N) => (p1

A. , A. <=, A. , and <. Exists, INT) : (j /= i AND 1 <= j AND j <= N) => (FORALL (t:INT) : (t /= j AND 1 <= t AND t <= N) => (p1

A. Nl1_aa, A. <=, <. N. And, and A. Exists, INT) : (j /= i AND 1 <= j AND j <= N AND k1 /= j) => (FORALL (t:INT) : (t /= j AND 1 <= t AND t <= N) => (p1, p.1

Q. Verification and %. Push, ASSERT N0_AA ; QUERY p[i].cs = 0 OR (p[i].cs = i)

Q. Exists, INT) : (1 <= j AND j <= N ) AND p[j].cs = 0 OR (p[j].cs = i)

<. , A. , and <. Forall, j:INT) : (j /= i AND 1 <= j AND j <= N) % AND (t[j], %NR1_A2 : BOOLEAN =

<. , A. , and <. Forall, j:INT) : (j /= i AND 1 <= j AND j <= N) % AND, %NR1_A21 : BOOLEAN =

<. , A. , and <. Forall, INT):(j /= i AND 1 <= j AND j <= N AND (t1[j].loc=1 OR t1[j].loc=2) AND (g1.loc = 0 OR g1.loc=1) AND ctl1, NR2_A21 : BOOLEAN =

<. , A. , and <. Forall, INT): (j /= i AND 1 <= j AND j <= N AND (t1[j].loc=1 OR t1[j].loc=2) AND (g1.loc = 1 OR g1.loc=2) AND ctl1, NL2_A21 : BOOLEAN =

%. Xtgs and %. Init, BOOLEAN = ctl.cnt=0 AND ctl.loc=0 AND g.loc=0 AND (1 <= i AND i <= N ) AND t[i].loc=0 AND t[i].c < 20 AND FORALL (j:INT) : j /= i AND (1 <= j AND j <= N)

%. %%%, near_j -> on_j) and (far_i -> near_i)

%. Push, ASSERT (t[i].loc = 0 OR t[i].loc= 1) AND (g.loc = 0 OR g.loc=1)

]. P. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, P. Habermehl et al., Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis, Proceedings 11th International Conference on Computer Aided Verification, CAV'99, pp.146-159, 1999.
DOI : 10.1007/3-540-48683-6_15

J. Abrial, The B-Book: Assigning Programs to Meanings, 1996.
DOI : 10.1017/CBO9780511624162

R. Alur and D. Dill, The theory of timed automata, Theoretical Computer Science, issue.126, pp.183-235, 1994.

H. Amjad, Combining model checking and theorem proving, pp.15-16, 2004.

M. Ammerlaan, R. L. Spelberg, and W. J. , XTG-an engineering approach to modelling and analysis of real-time systems, Proceeding. 10th EUROMICRO Workshop on Real-Time Systems (Cat. No.98EX168), pp.88-97, 1998.
DOI : 10.1109/EMWRTS.1998.685072

T. Amnell and M. Others, UPPAAL - Now, Next, and Future, Modeling and Verification of Parallel Processes, pp.99-124, 2001.
DOI : 10.1007/3-540-45510-8_4

URL : http://www.docs.uu.se/docs/rtmv/papers/movep2k.ps.gz

K. Apt and D. Kozen, Limits for automatic verification of finite-state concurrent systems, Information Processing Letters, vol.22, issue.6, 1986.
DOI : 10.1016/0020-0190(86)90071-2

E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli et al., Datastructures for the verification of timed automata, Proceedings of the 1st 171

T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani, Automatic predicate abstraction of c programs, Proceedings of the Programming Language Design and Implementation, pp.203-213, 2001.

T. Ball and S. K. Rajamani, The SLAM project: Debugging system software via static analysis, Principles of Programming Languages, pp.1-3, 2002.

T. Ball, R. Sriram, and K. , The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, pp.1-3, 2002.

G. Bandini, R. L. Spelberg, and H. Toetenel, Parametric model-checking in pmc

K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl, Abstracting WS1S Systems to Verify Parameterized Networks, Proceedings of the 6th Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pp.188-204, 2000.
DOI : 10.1007/3-540-46419-0_14

K. Baukus, Y. Lakhnech, and L. Stahl, Verifying Universal Properties of Parameterized Networks, 2000.
DOI : 10.1007/3-540-45352-0_24

S. Bensalem, Y. Lakhnech, and S. Owre, InVeSt : A tool for the verification of invariants, Proceedings 10th International Conference on Computer Aided Verification, CAV'98, pp.505-510, 1998.
DOI : 10.1007/BFb0028771

D. Cansell and D. Mery, Tutorial on the event-based B method, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00092846

D. Cansell, D. Mery, and S. Merz, Predicate Diagrams for the Verification of Reactive Systems, Proceedings the 2nd International Conference on Integrated Formal Methods, 1945.
DOI : 10.1007/3-540-40911-4_22

URL : https://hal.archives-ouvertes.fr/inria-00099125

D. Cansell, D. Mery, and S. Merz, Diagram refinements for the design of reactive systems, Journal of Universal Computer Science, vol.7, issue.2, pp.159-174, 2001.

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement, Proceedings 12th International Conference on Computer Aided Verification, CAV'00, pp.154-169, 2000.

E. M. Clarke and O. Grumberg, Avoiding the state explosion problem in temporal logic model checking, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing , PODC '87, pp.294-303, 1987.
DOI : 10.1145/41840.41865

M. Colon and T. E. Uribe, Generating finite-state abstractions of reactive systems using decision procedures, Computer Aided Verification, pp.293-304, 1998.
DOI : 10.1007/BFb0028753

P. Cousot and R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper, Proceedings of the International Workshop Programming Language Implementation and Logic Programming, PLILP '92, pp.13-17, 1992.

C. Homepage, Available at

D. Dams, Abstract Interpretation and Parition Refinement for Model Checking, 1996.

S. Das, Predicate Abstraction, 2004.

D. Dill and H. Wong-toi, Verification of real-time systems by successive over and under approximation, 7th CAV95, pp.409-422, 1995.
DOI : 10.1007/3-540-60045-0_66

L. Fejoz, D. Méry, and S. Merz, Dixit: a graphical toolkit for predicate abstractions, Intl. Workshop Automatic Verification of Infinite-State Systems (AVIS 2005), pp.39-48, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000767

C. Flanagan and S. Qadeer, Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002.

D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, On hte temporal analysis of fairness, ACM Symposium on principles of Programming Languages, pp.163-173, 1980.

S. Graf and H. Saidi, Construction of abstract state graphs with PVS, Proceedings 9th International Conference on Computer Aided Verification, CAV'97, pp.72-83, 1997.
DOI : 10.1007/3-540-63166-6_10

S. Graf and H. Saidi, Construction of abstract state graphs with PVS [32] N. Halbwachs. Delay analysis in synchronous programs, 9th CAV97 CAV93, pp.72-83, 1254.

K. Havelund and N. Shankar, Experimeents in theorem providing and model checking for protocol verification, FME, Lecture Notes in Computer Science, pp.662-681, 1996.

T. A. Henzinger and O. Kupferman, From quantity to quality, Proceedings of the 1st International Workshop on Hybrid and Real-Time Systems, 1997.
DOI : 10.1007/BFb0014712

T. A. Henzinger, P. Ho, and H. Wong-toi, HyTech: The Cornell Hybrid Technology Tool, proceedings of the 1st Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pp.29-43, 1995.
DOI : 10.1007/3-540-60472-3_14

T. A. Henzinger, R. Jhala, R. Majumdar, and K. Mcmillan, Abstractions from proofs, 31st Annual Symp. Princ. of Prog. Lang, 2004.
DOI : 10.1145/2641638.2641655

URL : http://www-cad.eecs.berkeley.edu/~tah/Publications/abstractions_from_proofs.ps

T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic model checking for real-time systems. information and computation, Information and Computation, pp.193-244, 1994.

E. Kang, Parametric analysis of real-time embedded systems with abstract approximation interpretation, 26th International Conference on Software Engineering, pp.39-41, 2004.

E. Kang, Real-time system verification techniques based on abstraction/deduction and model checking, Proceedings the 5th International Conference on Integrated Formal Methods, CS-Report 05-29, pp.26-32
URL : https://hal.archives-ouvertes.fr/inria-00000641

E. Kang and S. Merz, Predicate diagrams for the verification of real-time system, 5th International Workshop of Automated Verification of Critical Systems (AVoCS05), pp.151-165, 2005.

E. Kang and S. Merz, Predicate diagrams for the verification of real-time systems, Formal Aspects of Computing, vol.1, issue.1???2, pp.401-413, 2007.
DOI : 10.1007/3-540-60973-3_113

URL : https://hal.archives-ouvertes.fr/inria-00000631

K. J. Kristoffersen, F. Laroussinie, K. G. Larsen, P. Pettersson, and W. Yi, A compositional proof of a real-time mutual exclusion protocol, 1996.
URL : https://hal.archives-ouvertes.fr/hal-00904842

K. G. Larsen, P. Petterson, and W. Yi, Uppaal: Status & developments, 1997.
DOI : 10.1007/3-540-63166-6_47

URL : http://www.docs.uu.se/docs/rtmv/papers/lpw:cav97.ps.gz

D. Lesens, N. Halbwachs, and P. Raymond, Automatic verification of parameterized networks of processes, Theoretical Computer Science, vol.256, issue.1-2, pp.113-144, 2001.
DOI : 10.1016/S0304-3975(00)00104-3

URL : https://hal.archives-ouvertes.fr/hal-00198649

R. F. Spelberg, W. J. Toetenel, and M. Ammerlaan, Partition refinement in real-time model checking, Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp.143-157, 1998.
DOI : 10.1007/BFb0055344

Z. Manna and A. Pnueli, Verification of parameterized programs, 1995.

Z. Manna and A. Pnueli, Verification of parameterized programs: Specification and Validation Methods, 1994.

Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems:safety, 1995.

R. Milner, Communication and Concurrency, 1989.

J. Misra and K. M. Chandy, Parallel program design: a foundation, 1998.

S. Kedar, R. P. Namjoshi, and . Kurshan, Syntactic program transformations for automatic abstraction, Computer Aided Verification, pp.435-449, 2000.

C. Esti and N. , Predicate diagrams as Basis for the verification of reactive systems, 2004.

S. Graf and H. Saidi, Construction of abstract state graphs with PVS, Proc. 9th INternational Conference on Computer Aided Verification (CAV'97, pp.72-83, 1997.
DOI : 10.1007/3-540-63166-6_10

H. Sa, Modular and incremental analysis of concurrent software systems, 1999.

H. Sa¨?disa¨?di and N. Shankar, Abstract and model check while you prove, Computer-Aided Verification (CAV'99), number 1633 in Lecture Notes in Computer Science, pp.443-454, 1999.

R. Spelberg, Model Checking Real-Time Systems based on partition refinement, 2004.

S. Tripakis and S. Yovine, Analysis of timed systems based on timeabstracting bisimulations [58] P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants, Proceedings of the Eighth International Conference on CAV Proceedings of Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, pp.232-243, 1990.

Y. Kesten and A. Pnueli, Modularization and abstraction: The keys to practical formal verification, Proceedings of the 23th International Sumposium on Mathematical Foundations of Computer Science, pp.54-71, 1998.
DOI : 10.1007/BFb0055757

Y. Kesten and A. Pnueli, Modularization and abstraction: The keys to practical formal verification, 23th MFCS98, pp.54-71, 1450.
DOI : 10.1007/BFb0055757

S. Yovine, KRONOS: a??verification tool for real-time systems, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, 1997.
DOI : 10.1007/s100090050009