, Rodin: an open toolset for modelling and reasoning in Event-B. International journal on software tools for technology transfer, Abr10] Jean-Raymond Abrial. Modeling in Event-B -System and Software Engineering, pp.447-466, 2010.
, Subtyping dependent types, Theoretical Computer Science, vol.266, issue.1-2, pp.273-309, 2001.
DOI : 10.1016/S0304-3975(00)00175-4
URL : http://doi.org/10.1016/s0304-3975(00)00175-4
, Explicit Substitutions, Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '90, pp.31-46, 1990.
DOI : 10.1145/96709.96712
URL : https://hal.archives-ouvertes.fr/inria-00075382
, Combining the Coq proof assistant with first-order decision procedures, 2006.
, A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, 1st Intl. Conf. Certified Programs and Proofs, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130
, Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving, pp.83-98, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496
, The existence of refinement mappings, Theoretical Computer Science, vol.82, issue.2, pp.253-284, 1991.
DOI : 10.1016/0304-3975(91)90224-P
, On TLA as a Logic, Proceedings of the NATO Advanced Study Institute on Deductive Program Design, pp.235-271, 1996.
DOI : 10.1007/978-3-642-61455-2_14
, Proving assertions about parallel programs, J. Comput. Syst. Sci, vol.10, issue.1, pp.110-135, 1975.
, Subtyping with Power Types, Computer Science Logic, pp.156-171, 2000.
DOI : 10.1007/3-540-44622-2_10
, Eliminating definitions and Skolem functions in first-order logic, ACM Transactions on Computational Logic, vol.4, issue.3, pp.402-415, 2003.
DOI : 10.1145/772062.772068
, Computing Tiny Clause Normal Forms, Proceedings of the 24th International Conference on Automated Deduction, CADE'13, pp.109-125, 2013.
DOI : 10.1007/978-3-642-38574-2_7
URL : https://hal.archives-ouvertes.fr/hal-00931893
, The epsilon calculus The Stanford Encyclopedia of Philosophy, 2013.
, Automatic Proof and Disproof in Isabelle/HOL, Frontiers of Combining Systems, pp.12-27, 2011.
DOI : 10.1007/BFb0028402
, Extending Sledgehammer with SMT Solvers, Journal of automated reasoning, vol.37, issue.1-2, pp.109-128, 2013.
DOI : 10.1007/BFb0028402
, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS '99, pp.193-207, 1999.
DOI : 10.1007/3-540-49059-0_14
, Symbolic model checking: 1020 states and beyond, Inf. Comput, vol.98, issue.2, pp.142-170, 1992.
, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, Certified Programs and Proofs, pp.151-166, 2011.
DOI : 10.1016/j.jal.2007.07.003
URL : https://hal.archives-ouvertes.fr/hal-00646960
, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, 14th Intl. Conf. Logic for Programming, pp.151-165, 2007.
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920
, veriT: An Open, Trustable and Efficient SMT-Solver, Automated Deduction?CADE-22, pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634
, Completion without failure Resolution of equations in algebraic structures Rewrite-based equational theorem proving with selection and simplification, Journal of Logic and Computation, vol.2, issue.43, pp.1-30217, 1989.
, Resolution Theorem Proving, Handbook of Automated Reasoning, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.4450
, Semantic subtyping with an SMT solver, Proceedings of the 15th ACM SIGPLAN international conference on Functional programming , ICFP '10, pp.105-116, 2010.
, Minimal unsatisfiability and autarkies. Handbook of Satisfiability Monotonicity inference for higher-order formulas, Journal of Automated Reasoning, vol.185, issue.474, pp.339-401369, 2009.
, High-Level Specifications: Lessons from Industry, Formal Methods for Components and Objects, pp.242-261, 2003.
DOI : 10.1007/978-3-540-39656-7_10
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.6621
, Term rewriting and all that, 1999.
, Satisfiability Modulo Theories. Handbook of satisfiability, pp.825-885, 2009.
, The satisfiability modulo theories library (smt-lib). www.SMT-LIB.org, 2010.
, Experimenting with Deduction Modulo, Proceedings of the 23rd International Conference on Automated Deduction, pp.162-176, 2011.
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858
, Structural subtyping and the notion of power type, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '88, pp.70-79, 1988.
DOI : 10.1145/73560.73566
, Type systems, ACM Computing Surveys, vol.28, issue.1, pp.2208-2236, 1997.
DOI : 10.1145/234313.234418
, CC(X): Semantic Combination of Congruence Closure with Solvable Theories, Electronic Notes in Theoretical Computer Science, vol.198, issue.2, pp.51-69, 2008.
DOI : 10.1016/j.entcs.2008.04.080
, Verifying Safety Properties with the TLA???+??? Proof System, 5th Intl. Joint Conf. Automated Reasoning, pp.142-148, 2010.
DOI : 10.1007/978-3-642-14203-1_12
URL : https://hal.archives-ouvertes.fr/inria-00534821
, Soft typing, ACM SIGPLAN Notices, vol.26, issue.6, pp.278-292, 1991.
DOI : 10.1145/113446.113469
, Tuning the Alt-Ergo SMT solver for B proof obligations, Ameur and Schewe [AS14], pp.294-297
, Sort It Out with Monotonicity, Automated Deduction ? CADE-23, pp.207-221, 2011.
DOI : 10.1007/BF00243005
, A more expressive formulation of many sorted logic, Journal of automated reasoning, vol.3, issue.2, pp.113-200, 1987.
, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys, vol.17, issue.4, pp.471-523, 1985.
DOI : 10.1145/6041.6042
, Z3: An efficient SMT solver, 14th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
, Fourier-motzkin elimination and its dual, Journal of Combinatorial Theory, Series A, vol.14, issue.3, pp.288-297, 1973.
, Reasoning with triggers, 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, pp.22-31, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00703207
, The Yices SMT solver, 2006.
, DCAS is not a silver bullet for nonblocking algorithm design, Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures, SPAA '04, pp.216-224, 2004.
, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, Logic for Programming Artificial Intelligence and Reasoning (LPAR)LNCS)/Advanced Research in Computing and Software Science (ARCoSS), pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20
, The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations, Abstract State Machines, pp.290-293, 2014.
DOI : 10.1007/978-3-662-43652-3_26
URL : https://hal.archives-ouvertes.fr/hal-00998092
, Automatic Verification for a Class of Proof Obligations with SMT-Solvers, Abstract State Machines, pp.217-230, 2010.
DOI : 10.1007/978-3-642-11811-1_17
, Even Better DCAS-Based Concurrent Deques, Proceedings of the 14th International Conference on Distributed Computing, DISC '00, pp.59-73, 2000.
DOI : 10.1007/3-540-40026-5_4
, SMT Solvers for Rodin, 3rd Intl. Conf. Abstract State Machines, Alloy , B, VDM, and Z, pp.194-207, 2012.
DOI : 10.1007/978-3-642-30885-7_14
, Coalescing: Syntactic abstraction for reasoning in firstorder modal logics, Automated Reasoning in Quantified Non-Classical Logics, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01244623
, A survey of automated techniques for formal software verification, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, issue.7, pp.271165-1178, 2008.
, Memoir?Formal Specs and Correctness Proofs [dMB08] Leonardo de Moura and Nikolaj Bjorner. Proofs and refutations, and Z3, Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics CEUR Workshop Proceedings. CEUR-WS.org, 2008.
, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102
, A Mathematical Introduction to Logic, ch. 4.3 (Many-Sorted Logic, 2001.
, Hybrid type checking, ACM SIGPLAN Notices, vol.41, issue.1, pp.245-256, 2006.
DOI : 10.1145/1111320.1111059
, Assigning meanings to programs, Mathematical aspects of computer science, vol.19, pp.19-321, 1967.
DOI : 10.1090/psapm/019/0235771
, Appraising two decades of distributed computing theory research, Distrib. Comput, vol.16, issue.2-3, pp.239-247, 2003.
, Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, Tools and Algorithms for the Construction and Analysis of Systems, pp.167-181, 2006.
DOI : 10.1007/3-540-45620-1_26
URL : https://hal.archives-ouvertes.fr/inria-00001088
, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 Conf. on Programming language design and implementation, PLDI '91, pp.268-277, 1991.
, Combining Lists with Non-stably Infinite Theories, Logic for Programming, Artificial Intelligence , and Reasoning, pp.51-66, 2004.
DOI : 10.1007/978-3-540-32275-7_4
URL : https://hal.archives-ouvertes.fr/inria-00000481
, Solving quantified verification conditions using satisfiability modulo theories, Annals of Mathematics and Artificial Intelligence, vol.21, issue.2, pp.101-122, 2009.
DOI : 10.1007/s10472-009-9153-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.192.6628
, DPLL(T): Fast Decision Procedures, Computer aided verification, pp.175-188, 2004.
DOI : 10.1007/978-3-540-27813-9_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.8015
, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Proceedings of the 21st International Conference on Computer Aided Verification, CAV '09, pp.306-320, 2009.
DOI : 10.1007/978-3-642-02658-4_25
, Formal proof?the four-color theorem, Notices of the AMS, vol.55, issue.11, pp.1382-1393, 2008.
, A revision of the proof of the kepler conjecture, The Kepler Conjecture, pp.341-376, 2011.
, Generalizing Hindley-Milner type inference algorithms, 2002.
, Translating TLA???+??? to B for Validation with ProB, Lecture Notes in Computer Science, vol.7321, pp.24-38, 2012.
DOI : 10.1007/978-3-642-30729-4_3
, An axiomatic basis for computer programming, Commun . ACM, vol.12, issue.10, pp.576-580, 1969.
, Design and Validation of Computer Protocols
, The model checker spin, IEEE Transactions on software engineering, vol.23, issue.5, pp.279-295, 1997.
, Mars code, Commun. ACM, vol.57, issue.2, pp.64-73, 2014.
, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230
, First-order proof tactics in higher-order logic theorem provers, pp.56-68
, Software Abstractions: Logic, Language, and Analysis, 2012.
, Tableaux Modulo Theories Using Superdeduction, Proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR'12, pp.332-338, 2012.
DOI : 10.1007/978-3-642-31365-3_26
URL : https://hal.archives-ouvertes.fr/hal-01099338
, Solving equations in abstract algebras: A rule-based survey of unification, Computational Logic -Essays in Honor of Alan Robinson, pp.257-321, 1991.
, Proving SPARK Verification Conditions with SMT solvers, 2009.
, Simple word problems in universal algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
, sel4: Formal verification of an os kernel Type reconstruction for general refinement types, Proceedings of Bibliography the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, SOSP '09 Proceedings of the 16th European conference on Programming, ESOP'07, pp.207-220, 2007.
, Computeraided reasoning: an approach, 2000.
, A proposal for a theory of finite sets, lists, and maps for the smt-lib standard Efficient term-ite conversion for satisfiability modulo theories, Informal proceedings Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing, SAT '09, pp.195-208, 2009.
, Automated Reasoning Service for HOL Light, Intelligent Computer Mathematics Fundaments of branching heuristics. Handbook of Satisfiability, pp.120-135205, 2009.
DOI : 10.1007/978-3-642-39320-4_8
URL : http://repository.ubn.ru.nl/bitstream/2066/117154/1/117154.pdf
, Set theory, of Studies in Logic and the Foundations of Mathematics, 1980.
, Translation from set-theory to predicate calculus, 2012.
, First-Order Theorem Proving and Vampire, Computer Aided Verification, pp.1-35, 2013.
DOI : 10.1007/978-3-642-39799-8_1
, A new solution of Dijkstra's concurrent programming problem, Communications of the ACM, vol.17, issue.8, pp.453-454, 1974.
DOI : 10.1145/361082.361093
, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, vol.3, issue.2, pp.125-143, 1977.
DOI : 10.1109/TSE.1977.229904
, What good is temporal logic?, IFIP Congress, pp.657-668, 1983.
, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726
, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726
, How to Write a Proof, The American Mathematical Monthly, vol.102, issue.7, pp.600-608, 1995.
DOI : 10.2307/2974556
, Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers, 2002.
, Checking a Multithreaded Algorithm with ???+???CAL, Distributed Computing, pp.151-163, 2006.
DOI : 10.1007/11864219_11
, The +CAL algorithm language URL http://research. microsoft. com/users/lamport/tla/pluscal. html. The page can also be found by searching the Web for the, 2008.
, Byzantizing paxos by refinement Available at http://research.microsoft.com/en-us/um, 2011.
, Mathematics, form and function [lM93] Micha l Muzalewski. An outline of PC Mizar, 1986.
, Specifying and verifying systems with TLA+, Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC , EW10, pp.45-48, 2002.
DOI : 10.1145/1133373.1133382
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.5206
, Towards Verification of the Pastry Protocol Using TLA???+???, Formal Techniques for Distributed Systems, pp.244-258, 2011.
DOI : 10.1007/3-540-48153-2_6
URL : https://hal.archives-ouvertes.fr/inria-00593523
, Formal verification of Pastry using TLA +, International Workshop on the TLA+ Method and Tools, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00768812
, Should your specification language be typed, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, pp.502-526, 1999.
DOI : 10.1145/319301.319317
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.2302
, Distributed Algorithms, 1996.
, Extensions of First-Order Logic. Cambridge Tracts in Theoretical Computer Science, 2005.
, Towards a mathematical science of computation, IFIP Congress, pp.21-28, 1962.
, Metamath: A Computer Language for Pure Mathematics, 2007.
, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4
, Discharging Proof Obligations from Atelier??B Using Multiple Automated Provers, Proceedings of the Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ'12, pp.238-251, 2012.
DOI : 10.1007/978-3-642-30885-7_17
, Translating higher-order problems to first-order clauses, ESCoR (CEUR Workshop Proceedings, pp.70-80, 2006.
DOI : 10.1007/s10817-007-9085-y
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.573
, Translating Higher-Order Clauses to First-Order Clauses, Journal of Automated Reasoning, vol.9, issue.2, pp.35-60, 2008.
DOI : 10.1007/s10817-007-9085-y
, The Impact of Branching Heuristics in Propositional Satisfiability Algorithms, Progress in Artificial Intelligence, pp.62-74, 1999.
DOI : 10.1007/3-540-48159-1_5
, Conflict-driven clause learning sat solvers. Handbook of satisfiability, pp.131-153, 2009.
, Grasp: A search algorithm for propositional satisfiability. Computers, IEEE Transactions on, vol.48, issue.5, pp.506-521, 1999.
, Automatic Verification of TLA???+??? Proof Obligations with SMT Solvers, Lecture Notes in Computer Science, vol.7180, pp.289-303, 2012.
DOI : 10.1007/978-3-642-28717-6_23
URL : https://hal.archives-ouvertes.fr/hal-00760570
, Harnessing SMT Solvers for TLA + Proofs, ECEASST, vol.53, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00760579
, Refinement Types for tla ???+???, NASA Formal Methods, pp.143-157
DOI : 10.1007/978-3-319-06200-6_11
URL : https://hal.archives-ouvertes.fr/hal-01063516
, Why Amazon Chose TLA???+???, Ameur and Schewe [AS14], pp.25-39
DOI : 10.1007/978-3-662-43652-3_3
, Equational reasoning in Isabelle, Science of Computer Programming, vol.12, issue.2, pp.123-149, 1989.
DOI : 10.1016/0167-6423(89)90038-5
, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.2828
, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980.
DOI : 10.1145/322186.322198
, Proof-Producing Congruence Closure, Term Rewriting and Applications, pp.453-468, 2005.
DOI : 10.1007/978-3-540-32033-3_33
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.76.1716
, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.
DOI : 10.1145/1217856.1217859
, HOL: a proof assistant for higher-order logic, volume 2283 Theorem proving with ordering and equality constrained clauses, Journal of Symbolic Computation, vol.19, issue.4, pp.321-351, 1995.
, Computing Small Clause Normal Forms, Handbook of Automated Reasoning, pp.335-367, 2001.
DOI : 10.1016/B978-044450813-3/50008-4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.222
, PVS: An Experience Report, Proceedings of the International Workshop on Current Trends in Applied Formal Method: Applied Formal Methods, FM-Trends 98, pp.338-345, 1999.
DOI : 10.1007/3-540-48257-1_24
, Type inference with constrained types, Fourth International Workshop on Foundations of Object-Oriented Programming (FOOL), 1997.
DOI : 10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4
, Set theory for verification: I. from foundations to functions, J. Autom. Reasoning, vol.11, issue.3, pp.353-389, 1993.
, A generic tableau prover and its integration with Isabelle, Journal of Universal Computer Science, vol.5, issue.3, pp.73-87, 1999.
, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, PAAR@ IJCAR, pp.1-10, 2010.
, On the power of clauselearning SAT solvers with restarts, Principles and Practice of Constraint Programming-CP 2009, pp.654-668, 2009.
, Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, Journal of Automated Reasoning, vol.53, issue.6, pp.401-424, 2010.
DOI : 10.1007/s10817-009-9161-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.4794
, Myths about the mutual exclusion problem, Information Processing Letters, vol.12, issue.3, pp.115-116, 1981.
, Validating B,Z and TLA ???+??? Using ProB??and Kodkod, FM 2012: Formal Methods, pp.372-386, 2012.
DOI : 10.1007/978-3-642-32759-9_31
, Memoir: Practical state continuity for protected modules, Proceedings of the IEEE Symposium on Security and Privacy, 2011.
, The temporal logic of programs [Pot96] Francois Pottier. Simplifying subtyping constraints, Foundations of Computer Science 18th Annual Symposium on Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, pp.46-57, 1977.
, The essence of ML type inference, Advanced Topics in Types and Programming Languages, pp.389-489, 2005.
, The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing , Supercomputing '91, pp.4-13, 1991.
DOI : 10.1145/125826.125848
, A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA), Automated Reasoning, pp.453-467, 2006.
DOI : 10.1007/11814771_38
, Subtypes for specifications: predicate subtyping in PVS, IEEE Transactions on Software Engineering, vol.24, issue.9, pp.709-720, 1998.
DOI : 10.1109/32.713327
, Quantifier Instantiation Techniques for Finite Model Finding in SMT, Automated Deduction?CADE-24, pp.377-391, 2013.
DOI : 10.1007/978-3-642-38574-2_26
, Paramodulation and theorem-proving in firstorder theories with equality, Automation of Reasoning, Symbolic Computation, pp.298-313, 1983.
, The first-order theory of subtyping constraints, Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '02, pp.203-216, 2002.
, Lazy Satisfiability Modulo Theories, Journal on Satisfiability Boolean Modeling and Computation, 2007.
, Chord: A scalable peer-to-peer lookup service for internet applications, Proceedings of the 2001 Conference on Applications , Technologies, Architectures, and Protocols for Computer Communications , SIGCOMM '01, pp.149-160, 2001.
, Chord: a scalable peer-to-peer lookup protocol for internet applications, IEEE/ACM Transactions on Networking, vol.11, issue.1
DOI : 10.1109/TNET.2002.808407
, Subset Coercions in Coq, Types for Proofs and Programs, pp.237-252, 2007.
DOI : 10.1007/978-3-540-74464-1_16
URL : https://hal.archives-ouvertes.fr/inria-00628869
, The Z Notation: A Reference Manual, 1992.
, The TPTP Typed First-Order Form with Arithmetic, Lecture Notes in Computer Science, vol.7180, pp.406-419, 2012.
DOI : 10.1007/978-3-642-28717-6_32
, Type processing by constraint reasoning, Programming Languages and Systems, pp.1-25, 2006.
, System description: SystemOnTPTP. In Automated Deduction-CADE-17, pp.406-410, 2000.
, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8
, The TPTP World ??? Infrastructure for Automated Reasoning, Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'10, pp.1-12, 2010.
DOI : 10.1007/978-3-642-17511-4_1
, Logical types for untyped languages, ACM SIGPLAN Notices, vol.45, issue.9, pp.117-128, 2010.
DOI : 10.1145/1932681.1863561
, Logical types for untyped languages, Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, pp.117-128, 2010.
, Subtyping constrained types, Static Analysis, pp.349-365, 1996.
DOI : 10.1007/3-540-61739-6_52
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.5192
, On the complexity of derivation in propositional calculus . Studies in constructive mathematics and mathematical logic, pp.115-12510, 1968.
, Type inference for set theory, Theoretical Computer Science, vol.266, issue.1-2, pp.951-974, 2001.
DOI : 10.1016/S0304-3975(01)00123-2
, Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor, Proceedings of the 3rd IEEE International Workshop on Microprocessor Test and Verification (MTV '02, 2002.
, Translating Mizar for First Order Theorem Provers, Mathematical Knowledge Management, pp.203-215, 2003.
DOI : 10.1007/3-540-36469-2_16
, Automated reasoning for Mizar: Artificial intelligence through knowledge exchange, LPAR Workshops, 2008.
, Spass: Combining superposition, sorts and splitting. Handbook of automated reasoning, pp.1965-2013, 1999.
, Isabelle/Isar ?a generic framework for humanreadable proof documents. From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, pp.277-298, 2007.
, Mizars soft type system, Theorem Proving in Higher Order Logics, pp.383-399, 2007.
DOI : 10.1007/978-3-540-74591-4_28
, Formal methods, ACM Computing Surveys, vol.41, issue.4, pp.1-1936, 2009.
DOI : 10.1145/1592434.1592436
, The Isabelle Framework, 21st Intl. Conf. Theorem Proving in Higher Order Logics, pp.33-38, 2008.
DOI : 10.1007/978-3-540-74591-4_26
, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.214-227, 1999.
DOI : 10.1145/292540.292560
, Model Checking TLA+ Specifications, Correct Hardware Design and Verification Methods, pp.54-66, 1999.
DOI : 10.1007/3-540-48153-2_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.122.9499
, Using lightweight modeling to understand chord, ACM SIGCOMM Computer Communication Review, vol.42, issue.2, pp.49-57, 2012.
DOI : 10.1145/2185376.2185383
, How to make Chord correct. unpublished, 2014.
DOI : 10.1109/tse.2017.2655056
URL : http://arxiv.org/abs/1610.01140