We do not maintain this page any more.
Please visit our new web presence for up-to-date information.

Chair of Programming Methodology

Ádám Darvas

			Mailing address Ádám Darvas Software Engineering ETH Zentrum, RZ F3 8092 Zurich			Contact Office: RZ F3 Phone: +41 44 632 7951 Fax: +41 44 632 14 35 E-mail: Adam.Darvas at inf.ethz.ch

Overview

I am a research assistant at the Chair of Programming Methodology at ETH Zurich. I am doing my Ph.D. under the supervision of Peter Müller. Publications

Areas of interest: Formal methods and software verification, Software engineering, OO languages, Semantics, Java, JML, Spec#.

Teaching Assistance

Currently:

Software Engineering

Previously:	Introduction to Programming (HS 07)
	Concepts of object-oriented programming (WS 06/07 and AS 2008)
	Software Engineering (SS 2007 and SS 2006)
	Formal Methods and Functional Programming (SS 2005)
	Semantics of Programming Languages (SS 2004)
	IT Project Management (WS 05/06, WS 04/05 and WS 03/04)
	Software Engineering Seminar (WS 06/07)
	Specification and Verification of Object-oriented Software Seminar(WS 05/06, WS 04/05 and WS 03/04)
	References and Aliasing in Object-oriented Programs Seminar (SS 2004)

Student Supervision

HS 2007	David Steiger: Extending supported language subset of Jive
SS 06/07	Geraldine von Roten: Proving well-formedness of interface specifications
	Martin Bill: Usability Evaluation of Jive
SS 2006	Yoshimi Takano: Integrating Simplify into Jive
WS 05/06	Ronny Zakhejm: Ownership-based Program Verification in Jive
	Erich Laube: Design and Implementation of a JML Frontend for Boogie
SS 2005	Adrian Moos: Welldefinedness and expressiveness of JML specifications
WS 04/05	Ghislain Fourny: Generating Proof Obligations from JML Specifications
	Erich Laube: Transformation of Java Card into Diet Java Card
SS 2004	Marcello Miragliotta: Specification Model Library for the Interactive Program Prover JIVE

Publications

2008

Faithful mapping of model classes to mathematical structures [PDF] [BIB]
Ádám Darvas, and Peter Müller. In IET Software 2(6), 2008.
Efficient Well-Definedness Checking [PDF] [BIB] Springer-Online
Ádám Darvas, Farhad Mehta, and Arsenii Rudich. In IJCAR 2008, Sydney.
Checking Well-Formedness of Pure-Method Specifications [PDF] [BIB] Springer-Online
Arsenii Rudich, Ádám Darvas, and Peter Müller. In FM 2008, Turku.
Checking Well-Formedness of Pure-Method Specifications (Full Paper) [PDF] [BIB]
Arsenii Rudich, Ádám Darvas, and Peter Müller. Technical Report 588, ETH Zurich, 2008. Extension of FM paper with soundness proof.

2007

Faithful mapping of model classes to mathematical structures [PDF] [BIB]
Ádám Darvas and Peter Müller. In SAVCBS 2007, Dubrovnik.
Practical reasoning about invocations and implementations of pure methods [PDF] [BIB] Springer-Online
Ádám Darvas and K. Rustan M. Leino. In FASE 2007, Braga.
Formal encoding of JML Level 0 specifications in Jive [PDF] [BIB]
Ádám Darvas and Peter Müller. Technical Report 559, ETH Zurich, 2007.

2006

Reasoning About Method Calls in Interface Specifications [BIB] JOT-Online
Ádám Darvas and Peter Müller. In JOT 5(5), 2006.

2005

Reasoning About Method Calls in JML Specifications [PDF] [BIB]
Ádám Darvas and Peter Müller. In FTfJP 2005, Glasgow.
A Theorem Proving Approach to Analysis of Secure Information Flow [BIB] Springer-Online
Ádám Darvas, Reiner Hähnle, and Dave Sands. In SPC 2005, Boppard.

2003

A Theorem Proving Approach to Analysis of Secure Information Flow [PDF] [BIB]
Ádám Darvas, Reiner Hähnle, and Dave Sands. In WITS 2003, Warsaw.

2002

Model Checking of Replication Management [PDF] [BIB]
István Majzik and Ádám Darvas. In Supplement of EDCC-4 2002, Toulouse.
Verification of UML Statechart Models of Embedded Systems [PDF] [BIB]
Ádám Darvas, István Majzik, and Balázs Benyó. In IEEE DDESC 2002, Brno.