1. Backbone.js: a JavaScript library with a RESTful JSON interface. Available at
  2. Play: an open source MVC web application framework. Available at
  3. TypeScript: a language for application-scale JavaScript development, Available at
  4. Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak & Abhishek Udupa (2013): Syntax-Guided Synthesis. In: Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), doi:10.1109/FMCAD.2013.6679385.
  5. Ralph Back, Jim Grundy & Joakim Von Wright (1997): Structured Calculational Proof. Formal Aspects of Computing 9(5-6), pp. 469–483, doi:10.1007/BF01211456.
  6. Roland Backhouse & Diethard Michaelis (2006): Exercises in quantifier manipulation. In: Mathematics of program construction. Springer, pp. 69–81, doi:10.1007/11783596_7.
  7. Yves Bertot, Thomas Kleymann-Schreiber & Dilip Sequeira (1997): Implementing Proof by Pointing without a Structure Editor. Technical Report ECS-LFCS-97-368. University of Edinburgh. Available at
  8. Richard Bornat & Bernard Sufrin (1997): Jape: A calculator for animating proof-on-paper. In: Automated Deduction—CADE-14. Springer, pp. 412–415, doi:10.1007/3-540-63104-6_41.
  9. Michael Butler & Thomas Långbacka (1996): Program Derivation Using the Refinement Calculator. In: Theorem Proving in Higher Order Logics: 9th International Conference, volume 1125 of LNCS. Springer Verlag, pp. 93–108, doi:10.1007/BFb0105399.
  10. David Carrington, Ian Hayes, Ray Nickson, G. N. Watson & Jim Welsh (1996): A Tool for Developing Correct Programs by Refinement. Technical Report. Available at
  11. Dipak L. Chaudhari & Om Damani (2014): Automated Theorem Prover Assisted Program Calculations. In: Elvira Albert & Emil Sekerinski: Integrated Formal Methods, Lecture Notes in Computer Science. Springer International Publishing, pp. 205–220, doi:10.1007/978-3-319-10181-1_13.
  12. Dipak L. Chaudhari & Om Damani (2015): Introducing Formal Methods via Program Derivation. In: Innovation and Technology in Computer Science Education, ITiCSE 15.
  13. Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, MichałMoskal, Thomas Santen, Wolfram Schulte & Stephan Tobies (2009): VCC: A Practical System for Verifying Concurrent C. In: Theorem Proving in Higher Order Logics. Springer, doi:10.1007/978-3-642-03359-9_2.
  14. Edsger W. Dijkstra (1975): Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18(8), pp. 453–457, doi:10.1145/360933.360975.
  15. Edsger W. Dijkstra & W. H. Feijen (1988): A Method of Programming. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.
  16. Jean-Christophe Filliâtre & Andrei Paskevich (2013): Why3 – Where Programs Meet Provers. In: ESOP'13 22nd European Symposium on Programming, LNCS 7792. Springer, Rome, Italie, doi:10.1007/978-3-642-37036-6_8.
  17. Michael Franssen (1999): Cocktail: A tool for deriving correct programs. In: Workshop on Automated Reasoning.
  18. Bart Jacobs & Frank Piessens (2008): The VeriFast Program Verifier. Technical Report CW-520. Dept. of Computer Science, Katholieke Universiteit Leuven. Available at
  19. Anne Kaldewaij (1990): Programming: The Derivation of Algorithms. Prentice-Hall, Inc., NJ, USA.
  20. K. Rustan M. Leino (2010): Dafny: An Automatic Program Verifier for Functional Correctness. In: Logic for Programming, Artificial Intelligence, and Reasoning. Springer, doi:10.1007/978-3-642-17511-4_20.
  21. K. Rustan M. Leino (2011): Tools and Behavioral Abstraction: A Direction for Software Engineering. In: Sebastian Nanz: The Future of Software Engineering. Springer Berlin Heidelberg, pp. 115–124, doi:10.1007/978-3-642-15187-3_7.
  22. Marcel Oliveira, Manuela Xavier & Ana Cavalcanti (2004): Refine and Gabriel: support for refinement and tactics. In: Software Engineering and Formal Methods, 2004. SEFM 2004. Proceedings of the Second International Conference on. IEEE, pp. 310–319, doi:10.1109/SEFM.2004.1347535.
  23. Anthony M. Sloane (2011): Lightweight Language Processing in Kiama. In: JoãoM. Fernandes, Ralf Lämmel, Joost Visser & João Saraiva: Generative and Transformational Techniques in Software Engineering III, Lecture Notes in Computer Science 6491. Springer Berlin Heidelberg, pp. 408–425, doi:10.1007/978-3-642-18023-1_12.
  24. Douglas R. Smith (2008): Generating Programs Plus Proofs by Refinement. In: Bertrand Meyer & Jim Woodcock: Verified Software: Theories, Tools, Experiments, Lecture Notes in Computer Science 4171. Springer Berlin Heidelberg, pp. 182–188, doi:10.1007/978-3-540-69149-5_20.

Comments and questions to:
For website issues: