The existence of refinement mappings, Theor. Comput. Sci, vol.82, issue.2, pp.253-284, 1991. ,
Composing specifications, ACM Trans. Program. Lang. Syst, vol.15, issue.1, pp.73-132, 1993. ,
Open systems in TLA, Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, pp.81-90, 1994. ,
Conjoining specifications, ACM Trans. Program. Lang. Syst, vol.17, issue.3, pp.507-534, 1995. ,
The B-Book: Assigning Programs to Meanings, 1996. ,
Modeling in Event-B, 2010. ,
Defining liveness, Inf. Proc. Letters, vol.21, issue.4, pp.181-185, 1985. ,
Ten years of Hoare's logic: A survey -part 1, ACM Trans. Prog. Lang. and Syst, vol.3, issue.4, pp.431-483, 1981. ,
Fairness and hyperfairness in multi-party interactions, Distributed Computing, vol.6, issue.4, pp.245-254, 1993. ,
A machine-checked correctness proof for Pastry, Sci. Comput. Program, vol.158, pp.64-80, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01768758
On correct refinement of programs, J. Comp. and System Sci, vol.23, issue.1, pp.49-68, 1981. ,
Satisfiability modulo theories, Handbook of Model Checking, pp.305-343, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01095009
The Farsite project: a retrospective, Operating Systems Review, vol.41, issue.2, pp.17-26, 2007. ,
Zenon: An extensible automated theorem prover producing checkable proofs, 14th Intl. Conf. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), vol.4790, pp.151-165, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00315920
Program proving as hand simulation with a little induction, Information Processing, pp.308-312, 1974. ,
Formal verification of Multi-Paxos for distributed consensus, 21st Intl. Symp. Formal Methods (FM 2016), vol.9995, pp.119-136, 2016. ,
TLA + proofs, FM 2012: Formal Methods -18th International Symposium, vol.7436, pp.147-154, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00726631
A Discipline of Programming, 1976. ,
Protocol verification as a hardware design aid, IEEE Intl. Conf. Computer Design: VLSI in Computers and Processors, pp.522-525, 1992. ,
Coalescing: Syntactic abstraction for reasoning in first-order modal logics, Automated Reasoning in Quantified Non-Classical Logics, vol.33, pp.1-16, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01063512
Mechanical verification of concurrent systems with TLA, Computer Aided Verification, Fourth International Workshop, CAV '92, vol.663, pp.44-55, 1992. ,
Assigning meanings to programs, Proc. Symposium on Applied Mathematics, vol.19, pp.19-32, 1967. ,
A partial approach to model checking, Inf. Comput, vol.110, issue.2, pp.305-326, 1994. ,
Avoiding the undefined by underspecification, Computer Science Today, vol.1000, pp.366-373, 1995. ,
Evolving algebras 1993: Lipari guide, Specification and validation methods, pp.9-36, 1995. ,
Ironfleet: proving practical distributed systems correct, Proc. 25th Symp. Operating Systems Principles, SOSP 2015, pp.1-17, 2015. ,
Ironfleet: proving safety and liveness of practical distributed systems, Commun. ACM, vol.60, issue.7, pp.83-92, 2017. ,
The SPIN Model Checker, 2003. ,
Formal specification of a web services protocol, J. Log. Algebr. Program, vol.70, issue.1, pp.34-52, 2007. ,
Checking cache-coherence protocols with TLA + . Formal Methods in System Design, vol.22, pp.125-131, 2003. ,
LAR: A logic of algorithmic reasoning, Acta Informatica, vol.8, pp.243-266, 1977. ,
Proving the correctness of multiprocess programs, IEEE Trans. Software Eng, vol.3, issue.2, pp.125-143, 1977. ,
Time, clocks, and the ordering of events in a distributed system, Commun. ACM, vol.21, issue.7, pp.558-565, 1978. ,
A new approach to proving the correctness of multiprocess programs, ACM Trans. Program. Lang. Syst, vol.1, issue.1, pp.84-97, 1979. ,
Sometime" is sometimes "not never" -on the temporal logic of programs, Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, pp.174-185, 1980. ,
What good is temporal logic?, IFIP Congress, pp.657-668, 1983. ,
win and sin: Predicate transformers for concurrency, ACM Trans. Program. Lang. Syst, vol.12, issue.3, pp.396-428, 1990. ,
The Temporal Logic of Actions, Research Report, vol.79, 1991. ,
Hybrid systems in TLA +, Hybrid Systems, vol.736, pp.77-102 ,
, , 1992.
The temporal logic of actions, ACM Trans. Program. Lang. Syst, vol.16, issue.3, pp.872-923, 1994. ,
How to write a proof, American Mathematical Monthly, vol.102, issue.7, pp.600-608, 1995. ,
Fairness and hyperfairness, Distributed Computing, vol.13, issue.4, pp.239-245, 2000. ,
Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers, 2002. ,
The PlusCal algorithm language, Theoretical Aspects of Computing -ICTAC 2009, 6th International Colloquium, vol.5684, pp.36-60, 2009. ,
Byzantizing Paxos by refinement, Distributed Computing -25th International Symposium, vol.6950, pp.211-224, 2011. ,
The TLA + hyperbook, 2015. ,
, , 2018.
The TLA + video course, 2018. ,
Auxiliary variables in TLA + . CoRR, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01488617
Should your specification language be typed, ACM Trans. Program. Lang. Syst, vol.21, issue.3, pp.502-526, 1999. ,
The byzantine generals problem, ACM Trans. Program. Lang. Syst, vol.4, issue.3, pp.382-401, 1982. ,
Dafny: An automatic program verifier for functional correctness, 16th Intl. Conf. Logic for Programming, vol.6355, pp.348-370, 2010. ,
Checking that finite state concurrent programs satisfy their linear specification, Proc. Twelfth Ann. ACM Symp. Princ. Prog. Lang. (POPL 1985), pp.97-107, 1985. ,
Symbolic Model Checking, 1993. ,
A more complete TLA, FM'99: World Congress on Formal Methods, vol.1709, pp.1226-1244, 1999. ,
The specification language TLA +, Logics of Specification Languages, pp.401-451, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00338330
Programming from specifications, 1990. ,
How Amazon Web Services uses formal methods, CACM, vol.58, issue.4, pp.66-73, 2015. ,
Proving liveness properties of concurrent programs, ACM Trans. Program. Lang. Syst, vol.4, issue.3, pp.455-495, 1982. ,
Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol.828, 1994. ,
The temporal logic of programs, Proc. 18th Annual Symposium on the Foundations of Computer Science, pp.46-57, 1977. ,
, Past, Present and Future, 1967.
An interval-based temporal logic, Proc. Logics of Programs, vol.164, pp.443-457, 1984. ,
The Z Notation: A reference manual. International Series in Computer Science, 1992. ,
A PLTL-prover based on labelled superposition with partial model guidance, 6th Intl. Joint Conf. Automated Reasoning (IJCAR 2012, vol.7364, pp.537-543, 2012. ,
A stubborn attack on state explosion, 2nd Intl. Wsh. Computer Aided Verification, vol.531, pp.156-165, 1990. ,