, Proof General: A Generic Tool for Proof Development, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'00), pp.38-42, 2000.
DOI : 10.1007/3-540-46419-0_3
, A Tactic Language for Hiproofs, Proceedings of the 9th International Conference on Intelligent Computer Mathematics (AISC'08)
DOI : 10.1007/978-3-540-85110-3_30
, Interactive Theorem Proving and Program Development ? Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237
, Putting it all together ??? Formal verification of the VAMP, International Journal on Software Tools for Technology Transfer, vol.20, issue.2, pp.4-5, 2006.
DOI : 10.1112/S1461157000000176
, A distributed algorithm for strong bisimulation reduction of state spaces, International Journal on Software Tools for Technology Transfer, vol.10, issue.1, pp.74-86, 2005.
DOI : 10.1007/s001650050030
, Distributed Branching Bisimulation Minimization by Inductive Signatures, Proceedings of the 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'09)
DOI : 10.1007/s100090050018
URL : http://eprints.eemcs.utwente.nl/17088/01/0912.2550v1.pdf
, A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, 2013 IEEE 21st Symposium on Computer Arithmetic, pp.107-115, 2013.
DOI : 10.1109/ARITH.2013.30
URL : https://hal.archives-ouvertes.fr/hal-00743090
, A verification approach to applied system security, International Journal on Software Tools for Technology Transfer, vol.architecture, issue.3, pp.233-247, 2005.
DOI : 10.1007/3-540-45853-0_12
, Equivalence and Preorder Checking for Finite-State Systems, Handbook of Process Algebra, pp.391-424, 2001.
DOI : 10.1016/B978-044482830-9/50024-2
, A Storm is Coming: A Modern Probabilistic Model Checker, Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17), pp.592-600, 2017.
DOI : 10.1007/978-3-662-49674-9_8
URL : http://arxiv.org/pdf/1702.04311
, A Tactic Language for the System Coq, Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR'00), pp.85-95, 2000.
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070
, Coqoon -an IDE for interactive proof development in Coq, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), pp.316-331, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01242295
, Coqoon ? an ide for interactive proof development in Coq, Int. J. Softw. Tools Technol. Transf, pp.10009-10026, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01242295
, Automated verification of the FreeRTOS scheduler in Hip/Sleek, International Journal on Software Tools for Technology Transfer, vol.41, issue.1, pp.381-397, 2014.
DOI : 10.1007/s10703-012-0151-7
, Large-scale Distributed Verification Using CADP: Beyond Clusters to Grids, Proceedings of the 11th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'12). ENTCS, pp.145-161, 2013.
DOI : 10.1016/j.entcs.2013.07.010
URL : https://hal.archives-ouvertes.fr/hal-00730668
, Parallel state space construction for model-checking, Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'01), pp.217-234, 2001.
DOI : 10.1007/3-540-45139-0_14
URL : https://hal.archives-ouvertes.fr/inria-00072247
, The Four Colour Theorem: Engineering of a Formal Proof, Proceedings of the 8th Asian Symposium on Computer Mathematics (ASCM'07), p.333, 2007.
DOI : 10.1007/978-3-540-87827-8_28
, A Machine-Checked Proof of the Odd Order Theorem, Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP'13), pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699
, The Tinker tool for graphical tactic development, International Journal on Software Tools for Technology Transfer, vol.11, issue.3, 2017.
DOI : 10.1007/s001650050053
, Parallelizing the Spin Model Checker, Proceedings of the 19th International Workshop on Model Checking Software (SPIN'12), pp.155-171, 2012.
DOI : 10.1007/978-3-642-31759-0_12
, The Design of a Multicore Extension of the SPIN Model Checker, IEEE Transactions on Software Engineering, vol.33, issue.10, pp.659-674, 2007.
DOI : 10.1109/TSE.2007.70724
, Advances in Symbolic Probabilistic Model Checking with PRISM, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), pp.349-366, 2016.
DOI : 10.1007/978-3-662-49674-9_20
, Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic B??chi automata, International Journal on Software Tools for Technology Transfer, vol.47, issue.1, 2017.
DOI : 10.1007/978-3-642-37075-5_23
, PRISM 4.0: Verification of Probabilistic Real-Time Systems, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11), pp.585-591, 2011.
DOI : 10.1007/3-540-45657-0_17
URL : https://hal.archives-ouvertes.fr/hal-00648035
, PRISMgames 2.0: A tool for multi-objective strategy synthesis for stochastic games, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16)
, PRISMgames: Verification and strategy synthesis for stochastic multi-player games with multiple ob- jectives
DOI : 10.1007/s10009-017-0476-z
URL : https://link.springer.com/content/pdf/10.1007%2Fs10009-017-0476-z.pdf
, A Formal Proof of Cauchy???s Residue Theorem, Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP'16), pp.235-251, 2016.
DOI : 10.1007/978-3-642-59273-7
, Developing and Debugging Proof Strategies by Tinkering, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16)
DOI : 10.1007/978-3-662-49674-9_37
, PVS: A prototype verification system, Proceedings of the 11th International Conference on Automated Deduction (CADE'92)
DOI : 10.1007/3-540-55602-8_217
, Parallel algorithms for relational coarsest partition problems, IEEE Transactions on Parallel and Distributed Systems, vol.9, issue.7, pp.687-699, 1998.
DOI : 10.1109/71.707548
URL : http://www.engr.uconn.edu/~rajasek/Cmc2.pdf
, Parallel explicit model checking for generalized Büchi automata, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), pp.613-627, 2015.
, Parallelizing the Murphi verifier, Formal Methods in System Design, vol.18, issue.2, pp.117-129, 2001.
DOI : 10.1023/A:1008771324652
, Multi-core Decision Diagrams, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), pp.677-691, 2015.
DOI : 10.1145/155332.155354
, Multi-core symbolic bisimulation minimisation, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), pp.332-348, 2016.
, Multi-core symbolic bisimulation minimisation, Int. J. Softw. Tools Technol. Transf, 2017.
, Towards Informed Swarm Verification, Proceedings of the 3rd International Symposium on NASA Formal Methods (NFM'11), pp.422-437, 2011.
DOI : 10.1016/j.cie.2005.01.020
URL : http://www.win.tue.nl/~awijs/articles/informed_sv.pdf