Ádám Darvas

I used to be a research and teaching assistant at the Chair of Programming Methodology at ETH Zurich under the supervision of Peter Müller. I defended my PhD thesis and left ETH in September 2009.

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

Teaching Assistance

• Software Engineering (SS 2009, SS 2007 and SS 2006)
• Concepts of object-oriented programming (WS 06/07 and AS 2008)
• Formal Methods and Functional Programming (SS 2005)
• Introduction to Programming (HS 07)
  
• 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

Publications

(most of them available on the group's Publications page)

2010

• Proving Consistency and Completeness of Model Classes Using Theory Interpretation
  Ádám Darvas and Peter Müller. In FASE 2010, Paphos.

2009

• Reasoning about data abstraction in contract languages
  Ádám Darvas. Ph.D. Thesis, ETH Zurich, Diss. no. 18622, 2009.
  

2008

• Faithful mapping of model classes to mathematical structures
  Ádám Darvas and Peter Müller. In IET Software 2(6), 2008.
• Efficient Well-Definedness Checking
  Ádám Darvas, Farhad Mehta, and Arsenii Rudich. In IJCAR 2008, Sydney.
• Checking Well-Formedness of Pure-Method Specifications
  Arsenii Rudich, Ádám Darvas, and Peter Müller. In FM 2008, Turku. 
• Checking Well-Formedness of Pure-Method Specifications (Full Paper)
  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
  Ádám Darvas and Peter Müller. In SAVCBS 2007, Dubrovnik.
• Practical reasoning about invocations and implementations of pure methods
  Ádám Darvas and K. Rustan M. Leino. In FASE 2007, Braga.
• Formal encoding of JML Level 0 specifications in Jive
  Ádám Darvas and Peter Müller. Technical Report 559, ETH Zurich, 2007.

2006

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

2005

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

2003

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

2002

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