INT) : 1 <= i AND i <= N AND p[i] ,
INT) : 1 <= i AND i <= N AND (p1[i] ,
INT) : 1 <= i AND i <= N AND p[i] ,
BOOLEAN = FORALL (i:INT) : 1 <= i AND i <= N AND p[i] ,
BOOLEAN = (k1 = 0) AND (1 <= i AND i <= N) AND (p1[i] ,
BOOLEAN = (1 <= i AND i <= N) AND p1[i] ,
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) ,
INT) : (j /= i AND 1 <= j AND j <= N) => ( p1 ,
INT) : (j /= i AND 1 <= j AND j <= N) AND k1=j => ( FORALL (t:INT) : (t /= j AND 1 <= t AND t <= N) => ( p1 ,
INT) : (j /= i AND 1 <= j AND j <= N AND k1=j) => ( FORALL (t:INT) : (t /= j AND 1 <= t AND t <= N) => ( p1 ,
INT) : (j /= i AND 1 <= j AND j <= N) => (FORALL (t:INT) : (t /= j AND 1 <= t AND t <= N) => (p1 ,
INT) : (j /= i AND 1 <= j AND j <= N) => (FORALL (t:INT) : (t /= j AND 1 <= t AND t <= N) => (p1 ,
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 ,
ASSERT N0_AA ; QUERY p[i].cs = 0 OR (p[i].cs = i) ,
INT) : (1 <= j AND j <= N ) AND p[j].cs = 0 OR (p[j].cs = i) ,
j:INT) : (j /= i AND 1 <= j AND j <= N) % AND (t[j], %NR1_A2 : BOOLEAN = ,
j:INT) : (j /= i AND 1 <= j AND j <= N) % AND, %NR1_A21 : BOOLEAN = ,
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 = ,
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 = ,
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) ,
ASSERT (t[i].loc = 0 OR t[i].loc= 1) AND (g.loc = 0 OR g.loc=1) ,
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
The B-Book: Assigning Programs to Meanings, 1996. ,
DOI : 10.1017/CBO9780511624162
The theory of timed automata, Theoretical Computer Science, issue.126, pp.183-235, 1994. ,
Combining model checking and theorem proving, pp.15-16, 2004. ,
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
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
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
Datastructures for the verification of timed automata, Proceedings of the 1st 171 ,
Automatic predicate abstraction of c programs, Proceedings of the Programming Language Design and Implementation, pp.203-213, 2001. ,
The SLAM project: Debugging system software via static analysis, Principles of Programming Languages, pp.1-3, 2002. ,
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. ,
Parametric model-checking in pmc ,
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
Verifying Universal Properties of Parameterized Networks, 2000. ,
DOI : 10.1007/3-540-45352-0_24
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
Tutorial on the event-based B method, 2004. ,
URL : https://hal.archives-ouvertes.fr/inria-00092846
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
Diagram refinements for the design of reactive systems, Journal of Universal Computer Science, vol.7, issue.2, pp.159-174, 2001. ,
Counterexample-guided abstraction refinement, Proceedings 12th International Conference on Computer Aided Verification, CAV'00, pp.154-169, 2000. ,
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
Generating finite-state abstractions of reactive systems using decision procedures, Computer Aided Verification, pp.293-304, 1998. ,
DOI : 10.1007/BFb0028753
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. ,
Available at ,
Abstract Interpretation and Parition Refinement for Model Checking, 1996. ,
Predicate Abstraction, 2004. ,
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
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
Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002. ,
On hte temporal analysis of fairness, ACM Symposium on principles of Programming Languages, pp.163-173, 1980. ,
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
Construction of abstract state graphs with PVS [32] N. Halbwachs. Delay analysis in synchronous programs, 9th CAV97 CAV93, pp.72-83, 1254. ,
Experimeents in theorem providing and model checking for protocol verification, FME, Lecture Notes in Computer Science, pp.662-681, 1996. ,
From quantity to quality, Proceedings of the 1st International Workshop on Hybrid and Real-Time Systems, 1997. ,
DOI : 10.1007/BFb0014712
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
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
Symbolic model checking for real-time systems. information and computation, Information and Computation, pp.193-244, 1994. ,
Parametric analysis of real-time embedded systems with abstract approximation interpretation, 26th International Conference on Software Engineering, pp.39-41, 2004. ,
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
Predicate diagrams for the verification of real-time system, 5th International Workshop of Automated Verification of Critical Systems (AVoCS05), pp.151-165, 2005. ,
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
A compositional proof of a real-time mutual exclusion protocol, 1996. ,
URL : https://hal.archives-ouvertes.fr/hal-00904842
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
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
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
Verification of parameterized programs, 1995. ,
Verification of parameterized programs: Specification and Validation Methods, 1994. ,
Temporal Verification of Reactive Systems:safety, 1995. ,
Communication and Concurrency, 1989. ,
Parallel program design: a foundation, 1998. ,
Syntactic program transformations for automatic abstraction, Computer Aided Verification, pp.435-449, 2000. ,
Predicate diagrams as Basis for the verification of reactive systems, 2004. ,
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
Modular and incremental analysis of concurrent software systems, 1999. ,
Abstract and model check while you prove, Computer-Aided Verification (CAV'99), number 1633 in Lecture Notes in Computer Science, pp.443-454, 1999. ,
Model Checking Real-Time Systems based on partition refinement, 2004. ,
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. ,
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
Modularization and abstraction: The keys to practical formal verification, 23th MFCS98, pp.54-71, 1450. ,
DOI : 10.1007/BFb0055757
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