References

Disclaimer: this list has not been updated recently. For more references see the personal homepages of the members of the SoS group.

[ BergEtAl:WADT99]

Joachim van den Berg, Marieke Huisman, Bart Jacobs, Erik Poll, A Type-Theoretic Memory Model for Verification of Sequential Java Programs In: D. Bert, C. Choppy, and P.D. Mosses (eds.), Recent Trends in Algebraic Development Techniques, Springer LNCS 1827, 2000, p.1-21. © Springer-Verlag

[ BergJP:CJW2000]

Joachim van den Berg, Bart Jacobs, Erik Poll, Formal Specification and Verification of JavaCard's Application Identifier Class In: I. Attali and Th. Jensen (eds.), Java on Smart Cards: Programming and Security (Springer LNCS 2041, 2001) 137--150. © Springer-Verlag Proceedings of the Java Card 2000 Workshop

[ BergJ:TACAS01]

Joachim van den Berg, Bart Jacobs, The LOOP compiler for Java and JML In: T. Margaria and W. Yi (eds.), Tools and Algorithms for the Construction and Analysis of Software (TACAS), (Springer LNCS 2031, 2001) 299--312. © Springer-Verlag

[ BreunesseBJ02]

Cees-Bart Breunesse, Bart Jacobs, Joachim van den Berg, Specifying and Verifying an example: a decimal representation in Java for smart cards, to appear in the proceedings of the VerifiCard annual meeting.

[ Hensel:thesis]

Ulrich Hensel, Definition and Proof Principles for Data and Processes. Thesis, Techn. Univ. Dresden, 1999.

[ HenselEtAl:ETAPS98]

Ulrich Hensel, Marieke Huisman, Bart Jacobs, Hendrik Tews, Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools. In: Ch. Hankin (ed.), European Symposium on Programming, Springer LNCS 1381, 1998, p.105-121. © Springer-Verlag

[ HuismanJ:FASE00]

Marieke Huisman, Bart Jacobs, Java Program Verification via a Hoare Logic with Abrupt Termination. In: T. Maibaum (ed), Fundamental Approaches to Software Engineering (FASE'00), Springer LNCS 1783, p.284-303, 2000. © Springer-Verlag

[ HuismanJ:TPHOL00]

Marieke Huisman, Bart Jacobs, Inheritance in Higher Order Logic: Modeling and Reasoning. In: M. Aagaard and J. Harrison (eds.) Theorem Proving in Higher Order Logics (TPHOL) Springer LNCS 1869, p.301-319, 2000. © Springer-Verlag

[ HuismanEtAl:FTfJP99]

Marieke Huisman, Bart Jacobs, Joachim van den Berg, A case study in class library verification: Java's Vector class. Technical Report CSI-R0007, Computing Science Institute, University of Nijmegen.
An earlier version appeared in: B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter (eds.): Formal Techniques for Java Programs. Proceedings of the ECOOP'99 Workshop. Technical Report 251, Fernuniversität Hagen, 1999, p.37-44.

[ MeijerPoll:eSmart01]

Hans Meijer and Erik Poll, Towards a full formal specification of the Java Card API, In Smart Card Programming and Security, the proceedings of International Conference on Research in Smart Cards, E-smart 2001, Cannes, France, September 19-21, volume 2140 of LNCS, pages 165-178, Springer Verlag, 2001.

[Jacobs96]

Bart Jacobs, Objects and classes, co-algebraically. In: B. Freitag, C.B. Jones, C. Lengauer, and H.-J. Schek (eds) Object-Orientation with Parallelism and Persistence. Kluwer Acad. Publ., 1996, p. 83--103.

[ Jacobs:AMAST97]

Bart Jacobs, Invariants, Bisimulations and the Correctness of Coalgebraic Refinements. In: M. Johnson (ed), Algebraic Methodology and Software Technology, LNCS 1349, p.276-291, 1997. © Springer-Verlag

[ Jacobs:CMCS00]

Bart Jacobs, Towards a Duality Result Coalgebraic Modal Logic. Electr. Notes in Comp. Sci. 33, 2000. (Special issue on the workshop Coalgebraic Methods in Computer Science (CMCS 2000)).

[ Jacobs:TempLog99]

Bart Jacobs, The temporal logic of coalgebras via Galois algebras. Technical Report CSI-R9906, Computing Science Institute, University of Nijmegen, 1999. To appear in: Math. Struct. in Comp. Science.

[ Jacobs:MathFit00]

Bart Jacobs, Exercises in Coalgebraic Specification, manuscript, 1999.

[ Jacobs:ESOP01]

B. Jacobs, A Formalisation of Java's Exception Mechanism In: D. Sands (ed.), Programming Languages and Systems (ESOP), (Springer LNCS 2028, 2001), p.284-301. © Springer-Verlag

[ Jacobs:MSML]

Bart Jacobs, Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study Technical Report CSI-R0020, Computing Science Institute, University of Nijmegen.

[ JacobsEtAl:OOPSLA98]

Bart Jacobs, Joachim van den Berg, Marieke Huisman, Ulrich Hensel, Hendrik Tews, Reasoning about Java (Preliminary Report). Object-Oriented Programming Systems, Languages and Applications, ACM Press, 1998, p.329-340.

[ JacobsEtAl:NVTI01]

Bart Jacobs, Hans Meijer and Erik Poll, VerifiCard: A European Project for Smart Card Verification. In: Newsletter 5 of the Dutch Association for Theoretical Computer Science (NVTI), 2001

[ JacobsP:AMAST00]

Bart Jacobs, Erik Poll, A Monad for Basic Java Semantics. In: T. Rus (ed), Algebraic Methodology and Software Technology (AMAST'00), Springer LNCS 1816, p.150-164, 2000. © Springer-Verlag
An earlier version is available as Techn. Rep. CSI-R9926, Computing Science Institute, Univ. Nijmegen, 1999.

[ JacobsP:FASE01]

Bart Jacobs, Erik Poll, A Logic for the Java Modeling Language JML In: H. Hussmann (ed.), Fundamental Approaches to Software Engineering (FASE), (Springer LNCS 2029, 2001), p.284-299. © Springer-Verlag

[ JacobsR:EATCS97]

Bart Jacobs and Jan Rutten, A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin 62, 1997, p.222-259.

[ Lambooij]

Peter Lambooij, The YAPI protocol for buffered data transfer. A case study in object oriented specification and verification. Technical Report CSI-R9923, Computing Science Institute, University of Nijmegen.

[ LeavensEtAl:OOPSLA2000]

G.T. Leavens, K.R.M. Leino, E. Poll, C. Ruby, and B. Jacobs. JML: notations and tools supporting detailed design in Java. To appear in OOPSLA 2000 Companion, Minneapolis, Minnesota. Copyright ACM, 2000. Also Department of Computer Science, Iowa State University, TR #00-15, August 2000

[ Poll:CMCS00]

Erik Poll, A Coalgebraic Semantics of Subtyping. Electr. Notes in Comp. Sci. 33, 2000. (Special issue on the workshop Coalgebraic Methods in Computer Science (CMCS 2000)).

[ PollBJ:CARDIS00]

Erik Poll, Joachim van den Berg, Bart Jacobs, Specification of the JavaCard API in JML. In: J. Domingo-Ferrer and D. Chan and A. Watson (eds.), Smart Card Research and Advanced Application (IFIP Cardis 2000) (Kluwer Acad. Publ. 2000), p.135--154

[ PollBJ:CN01]

Erik Poll, Joachim van den Berg, Bart Jacobs, Formal Specification of the JavaCard API in JML: the APDU class. Computer Networks 36(4) (2001) p.407-421. It is the journal version of [PollBJ:CARDIS00].

[ PollZ:TLCA99]

Erik Poll and Jan Zwanenburg. A logic for abstract data types as existential types. In: J.-Y. Girard (ed), Typed Lambda Calculi and Applications (TLCA'99), LNCS 1581, 1999, p.310-324.

[ Reichel:MSCS95]

Horst Reichel, An approach to object semantics based on terminal co-algebras, Mathematical Structures in Computer Science 5 (1995), p.129-152.

[ RotheBT:JUCS01]

J. Rothe, B. Jacobs, H. Tews, The Coalgebraic Class Specification Language CCSL. Journal of Universal Computer Science, 7(2), 2001.

[ Tews:CCSL-Lang]

Hendrik Tews, Coalgebraic Class Specification Language (Reference Manual), manuscript, July, 1998.

[ Tews:CMCS00]

Hendrik Tews, Coalgebras for Binary Methods. Electr. Notes in Comp. Sci. 33, 2000. (Special issue on the workshop Coalgebraic Methods in Computer Science (CMCS 2000)).