Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology, vol.5, issue.3, pp.231-261, 1996. ,
DOI : 10.1145/234426.234431
ACL2: an industrial strength version of Nqthm, Proceedings of 11th Annual Conference on Computer Assurance. COMPASS '96, 1996. ,
DOI : 10.1109/CMPASS.1996.507872
PVS: A prototype verification system, 11th International Conference on Automated Deduction (CADE), ser. Lecture Notes in Artificial Intelligence, pp.748-752, 1992. ,
DOI : 10.1007/3-540-55602-8_217
Introduction to HOL: A Theorem- Proving Environment for Higher-Order Logic, 1993. ,
Isabelle: a Generic Theorem Prover, ser. Lecture Notes in Computer Science, 1994. ,
DOI : 10.1007/BFb0030541
The software model checker Blast, International Journal on Software Tools for Technology Transfer, vol.2, issue.4, pp.505-525, 2007. ,
DOI : 10.1007/s10009-007-0044-z
NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Computer Aided Verification, pp.359-364, 2002. ,
DOI : 10.1007/3-540-45657-0_29
PRISM: A Tool for Automatic Verification of Probabilistic Systems, Lecture Notes in Computer Science, vol.3920, pp.441-444, 2006. ,
DOI : 10.1007/11691372_29
The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997. ,
DOI : 10.1109/32.588521
NASA Langley's research and technology-transfer program in formal methods, COMPASS '95 Proceedings of the Tenth Annual Conference on Computer Assurance Systems Integrity, Software Safety and Process Security', pp.135-149, 1995. ,
DOI : 10.1109/CMPASS.1995.521893
An industrial strength theorem prover for a logic based on Common Lisp, IEEE Transactions on Software Engineering, vol.23, issue.4, pp.203-213, 1997. ,
DOI : 10.1109/32.588534
Industrial applications of model checking in Modeling and Verification of Parallel Processes, ser. Lecture Notes in Computer Science, pp.153-168, 2001. ,
Model checking in industrial hardware design, Proceedings of the 32nd ACM/IEEE conference on Design automation conference , DAC '95, pp.298-303, 1995. ,
DOI : 10.1145/217474.217545
Understanding Z: a specification language and its formal semantics, 1988. ,
CoreASM: An Extensible ASM Execution Engine, Fundam. Inf, vol.77, issue.12, pp.71-103, 2007. ,
A Metamodel-based Language and a Simulation Engine for Abstract State Machines, pp.1949-1983, 2008. ,
VDMTools: Advances in Support for Formal Modeling in VDM, SIGPLAN Not, vol.43, issue.2, pp.3-11, 2008. ,
ProB: an automated analysis toolset for the B method, International Journal on Software Tools for Technology Transfer, vol.49, issue.3, pp.185-203, 2008. ,
DOI : 10.1007/s10009-007-0063-9
Software Abstractions: Logic, Language, and Analysis, 2006. ,
Transformation Heuristics for Formal Requirements Validation by Animation, 2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems (SafeCert'09), 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00374082
Stepwise Validation of Formal Specifications, 2011 18th Asia-Pacific Software Engineering Conference, 2011. ,
DOI : 10.1109/APSEC.2011.48
URL : https://hal.archives-ouvertes.fr/inria-00392939
On Formalism in Specifications, IEEE Software, vol.2, issue.1, pp.6-26, 1985. ,
DOI : 10.1109/MS.1985.229776
Guidelines for Formal Domain Modeling in Event-B, 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, pp.138-145, 2011. ,
DOI : 10.1109/HASE.2011.47
URL : https://hal.archives-ouvertes.fr/hal-00640203
Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977. ,
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790
BRAMA: A New Graphic Animation Tool for B Models, " in B 2007: Formal Specification and Development in B, pp.274-276, 2006. ,
Formal Domain Engineering: From Specification to Validation, 2011. ,
URL : https://hal.archives-ouvertes.fr/tel-00614269
An Open Extensible Tool Environment for Event-B, Proceedings of the 8th international conference on Formal Methods and Software Engineering, ser. ICFEM'06, pp.588-605, 2006. ,
DOI : 10.1007/11901433_32
B Evénementiel pour la Modélisation du Domaine: Application au Transport, Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'09), pp.1-19, 2009. ,
Domain Engineering with Event-B: Some Lessons We Learned, 2010 18th IEEE International Requirements Engineering Conference, pp.252-261, 2010. ,
DOI : 10.1109/RE.2010.37
URL : https://hal.archives-ouvertes.fr/inria-00431133
The landing gear system case study The Landing Gear Case Study, ser. Communications in Computer and Information Science, ABZ 2014, pp.1-18, 2014. ,
Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles, 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008. ,
DOI : 10.1109/TASE.2008.39
URL : https://hal.archives-ouvertes.fr/hal-00260577
Longitudinal and lateral servoing of vehicles in a platoon, Proceedings of Conference on Intelligent Vehicles, pp.41-46, 1996. ,
DOI : 10.1109/IVS.1996.566349
Safe longitudinal platoons of vehicles without communication, 2009 IEEE International Conference on Robotics and Automation, 2008. ,
DOI : 10.1109/ROBOT.2009.5152629
URL : https://hal.archives-ouvertes.fr/inria-00342719
Towards Validating a Platoon of Cristal Vehicles using CSPB, 12th International Conference on Algebraic Methodology and Software Technology, pp.139-144, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00261630
Towards correct executable semantics for Z, " in Z User Workshop, Cambridge 1994, ser. Workshops in Computing, pp.185-209, 1994. ,
Animating Z: interactivity, transparency and equivalence, Proceedings 1995 Asia Pacific Software Engineering Conference, pp.294-303, 1995. ,
DOI : 10.1109/APSEC.1995.496978
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.6111
The Sage System Architecture: A System for the Rapid Development of Graphics Interfaces for Decision Support, IEEE Computer Graphics and Applications, vol.5, issue.11, pp.38-50, 1985. ,
DOI : 10.1109/MCG.1985.276330
A declarative approach to visualizing concurrent computations, Computer, vol.22, issue.10, pp.25-36, 1989. ,
DOI : 10.1109/2.42012
Specifications are not (necessarily) executable, Software Engineering Journal, vol.4, issue.6, pp.330-338, 1989. ,
DOI : 10.1049/sej.1989.0045
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.5087
Specifications are (preferably) executable, Software Engineering Journal, vol.7, issue.5, pp.323-334, 1992. ,
DOI : 10.1049/sej.1992.0033
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.1036
Specification and transformation of programs: a formal approach to software development, 1990. ,
DOI : 10.1007/978-3-642-61512-2
The Case for Using Simulation to Validate Event-B Specifications, 2012 19th Asia-Pacific Software Engineering Conference, pp.85-90, 2012. ,
DOI : 10.1109/APSEC.2012.66
URL : https://hal.archives-ouvertes.fr/hal-00772812