Ralph-Johan Back (2009):
Invariant Based Programming: Basic approach and Teaching Experiences.
Formal Aspects of Computing 21(3),
pp. 227–244,
doi:10.1007/s00165-008-0070-y.
Ralph-Johan Back, Johannes Eriksson & Linda Mannila (2007):
Teaching the Construction of Correct Programs Using Invariant Based Programming.
In: Proc. of SEEFM 2007.
South-East European Research Centre,
pp. 171–187.
Ralph-Johan Back, Johannes Eriksson & Magnus Myreen (2007):
Testing and Verifying Invariant Based Programs in the SOCOS Environment.
In: Proc. of Tests and Proofs (TAP) 2007,
LNCS 4454.
Springer,
pp. 61–78,
doi:10.1007/978-3-540-73770-4_4.
Ralph-Johan Back & Magnus Myreen (2005):
Tool Support for Invariant Based Programming.
In: Proc. of APSEC 2005.
IEEE Computer Society,
pp. 711–718,
doi:10.1109/APSEC.2005.104.
Ralph-Johan Back & Viorel Preoteasa (2011):
Semantics and Proof Rules of Invariant Based Programs.
In: 26th Symposium On Applied Computing,
pp. 1658–1665,
doi:10.1145/1982185.1982532.
Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs & K. Rustan M. Leino (2006):
Boogie: A modular reusable verifier for object-oriented programs.
In: Proc. of FMCO 2005,
LNCS 4111.
Springer,
pp. 364–387,
doi:10.1007/11804192_17.
Mike Barnett, K. Rustan M. Leino & Wolfram Schulte (2004):
The Spec# programming system: An overview.
In: CASSIS 2004,
LNCS 3362.
Springer,
pp. 49–69,
doi:10.1007/978-3-540-30569-9_3.
Joachim van den Berg & Bart Jacobs (2001):
The LOOP Compiler for Java and JML.
In: Proc. of TACAS 2001,
LNCS 2031.
Springer,
pp. 299–312,
doi:10.1007/3-540-45319-9_21.
Thomas H. Cormen, Clifford Stein, Ronald L. Rivest & Charles E. Leiserson (2001):
Introduction to Algorithms.
MIT Press.
David Detlefs, Greg Nelson & James B. Saxe (2005):
Simplify: a theorem prover for program checking.
Journal of the ACM 52(3),
pp. 365–473,
doi:10.1145/1066100.1066102.
Bruno Dutertre & Leonardo de Moura (2006):
The Yices SMT solver.
Technical Report.
Computer Science Laboratory, SRI International,
Menlo Park, CA.
Available at http://yices.csl.sri.com/tool-paper.pdf.
M. H. van Emden (1979):
Programming with Verification Conditions.
IEEE Transactions on Software Engineering 5(2),
pp. 148–159,
doi:10.1109/TSE.1979.234171.
Johannes Eriksson & Ralph-Johan Back (2010):
Applying PVS Background Theories and Proof Strategies in Invariant Based Programming.
In: Proc. of ICFEM 2010,
pp. 24–39,
doi:10.1007/978-3-642-16901-4_4.
Jean-Christophe Filliâtre & Claude Marché (2007):
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification.
In: Proc. of CAV 2007,
LNCS 4590.
Springer,
pp. 173–177,
doi:10.1007/978-3-540-73368-3_21.
Sam Owre, S. Rajan, John Rushby, Natarajan Shankar & Mandayam K. Srivas (1996):
PVS: Combining specification, proof checking, and model checking.
In: Proc. of CAV'96,
LNCS 1102.
Springer,
pp. 411–414,
doi:10.1007/3-540-61474-5_91.
Sam Owre & Natarajan Shankar (1997):
The Formal Semantics of PVS.
Technical Report SRI-CSL-97-2.
Computer Science Laboratory, SRI International,
Menlo Park, CA.
Available at http://www.csl.sri.com/papers/csl-97-2.
John C. Reynolds (1978):
Programming with transition diagrams.
In: D. Gries: Programming Methodology.
Springer-Verlag,
pp. 153–165.
John Rushby, Sam Owre & N. Shankar (1998):
Subtypes for Specifications: Predicate Subtyping in PVS.
IEEE Transactions on Software Engineering 24(9),
pp. 709–720,
doi:10.1109/32.713327.
eptcs@eptcs.org