Alexander Malkis

La información de esta página podría estar desactualizada debido a que Alexander Malkis no es actualmente miembro del Instituto.

PhD - Universidad de Friburgo, Alemania
Antiguo Post-doctoral Researcher

Página web: https://wwwbroy.in.tum.de/~malkis/index.htm

Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Current status

Moved to Technische Universität München.

Teaching

Model-checking lecture, TU Munich, SS 2012.
Supervision of Bachelor and PhD students (Jan Leike, Marco Muniz), Uni Freiburg, WS 2009-10.
Verification lecture, Uni Freiburg, WS 2007-08.
Seminar: Abstract Interpretation, Uni Freiburg, WS 2007-08.
Seminar: Advanced topics in Model Checking, Uni Freiburg, SS 2007.
Seminar: Software Model Checking, Uni Freiburg, WS 2006-07.
Seminar: Software Model Checking, MPII, SS 2005.
Reading Group at MPII, WS 2005 - SS 2006.

Publications

Verification Of Software Barriers, Alexander Malkis, Anindya Banerjee; PPoPP 2012, New Orleans, ACM. The web site contains all the details.
On the Strength of Owicki-Gries for Resources, Alexander Malkis, Laurent Mauborgne; APLAS 2011, Kenting, Springer. The technical report contains all the proofs.
A Practical Generic Privacy Language, Moritz Becker, Alexander Malkis, Laurent Bussard; ICISS 2010, Gandhinagar, Springer. Participation funded by IMDEA and ICISS 2010. Slides.
Thread-Modular Counterexample-Guided Abstraction Refinement, Alexander Malkis, Andreas Podelski, Andrey Rybalchenko; SAS 2010, Perpignan, Springer.
Cartesian Abstraction and Verification of Multithreaded Programs, PhD thesis, University of Freiburg, defended in 2010. Referees: A. Podelski, E.-R. Olderog.
Refinement With Exceptions, Alexander Malkis, Andreas Podelski; technical report, University of Freiburg, 2009.
Abstract Threads, Alexander Malkis, Shaz Qadeer, Shuvendu Lahiri; VMCAI 2010, Madrid, Springer. Its long version contains all the proofs. Conference participation partially funded by SIGPLAN PAC.
S4P: A Generic Language for Specifying Privacy Preferences and Policies, Moritz Y. Becker, Alexander Malkis, Laurent Bussard; Technical report MSR-TR-2010-32, Microsoft Research.
A Framework for Privacy Preferences and Data-Handling Policies, Moritz Y. Becker, Alexander Malkis, Laurent Bussard; Technical report MSR-TR-2009-128, Microsoft Research.
Precise Thread-Modular Verification, Alexander Malkis, Andreas Podelski, Andrey Rybalchenko; SAS 2007, Kongens Lyngby, Springer. A long version is available: Thread-Modular Verification with Arbitrary Precision.
Thread-Modular Verification is Cartesian Abstract Interpretation, Alexander Malkis, Andreas Podelski, Andrey Rybalchenko; ICTAC 2006, Tunis, Springer. Its long version Thread-Modular Verification and Cartesian Abstraction was presented at the TV 2006 workshop in Seattle.
Polyominoes, polyedges and the “Digit” game, Diploma thesis, Saarbrücken, 2004. Supervisor: R. Seidel.
Ещё раз о компьютеризации, А. Малкис; Энергетик, 9, 1997, ISSN 0013-7278. My first invited article. Published thanks to Адольф Ушерович Липец.

I am awarding discovering errors in my publications.

Invited tutorials

Modular verification of multithreaded shared-memory programs. September 2011, Prometidos-CM summer school, Madrid.
Verification of shared-memory multithreaded programs. December 2010, ICISS 2010, Gandhinagar, Gujarat, India.

Talks


Jan 2011	EPFL, Lausanne,	Counterexample-Guided Thread-Modular Verification
Dec 2010,	ICISS'10, Gandhinagar,	A Practical Generic Privacy Language
Sep 2010,	SAS'10, Perpignan,	Counterexample-Guided Thread-Modular Verification
Mar 2010,	IMDEA, Madrid,	Verification of Multithreaded Programs
Jan 2010,	VMCAI'10, Madrid,	Abstract Threads
Dec 2009,	UPMARC, Uppsala,	Owicki-Gries, Thread-Modular-Reasoning, Cartesian Abstraction
Oct 2009,	ARM, Cambridge,	Verification of Multithreaded Programs
Oct 2009,	Cambridge University,	Owicki-Gries, Thread-Modular-Reasoning, Cartesian Abstraction
Oct 2009,	Cambridge University,	Abstract Threads
Jun 2009,	MSR Cambridge,	SecPAL4Privacy
Feb 2009,	EPFL, Lausanne,	Counterexample-Guided Thread-Modular Verification
Sep 2008,	Freiburg University,	Cartesian Abstraction Refinement
Aug 2008,	ICMS, Edinburgh,	Cartesian Abstraction Refinement
Jul 2008,	MSR Redmond,	Concurrent Histories
May 2008,	MSR Redmond,	Cartesian Abstraction Refinement
Aug 2007,	SAS'07, Denmark,	Precise Thread-Modular Verification
Mar 2007,	EPFL, Lausanne,	Precise Thread-Modular Verification
Nov 2006,	ICTAC'06, Tunis,	Thread-Modular Verification is Cartesian Abstract Interpretation.

Tools

Improvements for Jahob specific to multithreaded programs.
AMTV: Automated Modular Thread Verifier. Checks safety of multithreaded programs. Licence: GPLv3.
XAHA for Boogie: eXperimental Automatic History Abstraction. Bounded safety verifier for multithreaded programs written in Boogie.
The Digit game. A human-computer turn-based logical game.

Reviewed for

VMCAI'06, PLDI'07, SAS'07, CAV'08, POPL'08, FMCAD'08, SOFSEM'09, TACAS'09, VMCAI'09, CAV'09, LICS'10, POPL'10, ESOP'11, FM'11, SOFSEM'11, CAV'11, VMCAI'11, POST'12, FACS'12

Research Interests

Program analysis, verification, concurrency, model-checking, abstract interpretation, assume-guarantee reasoning, modularity, compositionality, simulation, refinement, privacy, security, combinatorics, enumeration, polyforms.