Alexander Malkis

Contact

Photo of Alexander Malkis Institut für Informatik (I4)
Technische Universität München
Boltzmannstr. 3
85748 Garching bei München, Germany

E-mail: my_first_name dot my_last_name at tum dot de

Current status

My curriculum vitae is available at request.

Research interests

Software verification and program analysis:
- Concurrency: modularity, compositionality, model-checking of multithreaded programs, thread abstractions, recursion.
- Abstract interpretation: smooth refinement and completeness.
- Synchronization protocols: barriers.
- Theorem proving: cardinalities of set comprehensions.
Privacy and security:
- Specification languages, formal models, logic, policies and preferences, privacy-enabled dynamic networks.
- Access control, delegation, authorization.
- Provably secure architectures.
Combinatorics: enumeration, the diameter of transition graphs.

Teaching

Seminar: Algebraic methods and algorithms in cryptology, TU München, summer 2017.
Partially supporting the lecture Grundlagen Betriebssysteme und Systemsoftware, TU München, winter 2016–17.
Seminar: Prime numbers: Complexity and Algorithms, TU München, winter 2016–17. Main qualification exercises. Qualification exercises for the waiting list.
Seminar: Petri nets, TU München, winter 2016–17. Main qualification exercises. Qualification exercises for the waiting list.
Lecture support: Foundations of program and system development, TU München, winter 2014–15.
Lecture support: Foundations of program and system development, TU München, winter 2013–14.
Lecture support: Modeling distributed systems, TU München, summer 2013.
Lecture support: Foundations of software and system development, TU München, winter 2012–13.
Lecture: Model-checking, TU München, summer 2012.
Seminar: Verification of Concurrent Programs, TU München, summer 2012.
Short supervision of Bachelor and PhD students (Jan Leike, Marco Muñiz), Uni Freiburg, winter 2009–10.
Verification lecture, Uni Freiburg, winter 2007–08.
Seminar: Abstract Interpretation, Uni Freiburg, winter 2007–08.
Seminar: Advanced topics in Model Checking, Uni Freiburg, summer 2007.
Seminar: Software Model Checking, Uni Freiburg, winter 2006–07.
Seminar: Software Model Checking, MPII, summer 2005.
Reading Group, MPII, winter 2005 – summer 2006.

Publications

Contributed to: Logische und Methodische Grundlagen der Entwicklung verteilter Systeme, Manfred Broy unter Mitarbeit von Alexander Malkis; 2023, Softcover ISBN 978-3-662-67316-4, eBook ISBN 978-3-662-67317-1, Springer, DOI 10.1007/978-3-662-67317-1.
Reachability in Parallel Programs Is Polynomial in the Number of Threads, Alexander Malkis; JPDC, vol. 162, April 2022, pp. 1–16 (with typos as of 2022-01-18). Its long version [PDF] [PS] contains all the proofs (and, to the best of my knowledge, has no typos as of 2022-01-18).
Formal Methods: From Academia to Industrial Practice – A Travel Guide, Marieke Huisman, Dilian Gurov, and Alexander Malkis; arXiv.org > cs > arXiv:2002.07279, 2020.
Reachability in Multithreaded Programs Is Polynomial in the Number of Threads, Alexander Malkis; PDCAT'19, Gold Coast, Australia, © IEEE. Excerpt from the conference program. Details are in the accompanying technical report [PDF] [PS].
Contributed to: Logische und Methodische Grundlagen der Programm- und Systementwicklung: Datenstrukturen, funktionale, sequenzielle und objektorientierte Programmierung, Manfred Broy unter Mitarbeit von Alexander Malkis; 2019, Softcover ISBN 978-3-658-26301-0, eBook ISBN 978-3-658-26302-7, Springer, DOI 10.1007/978-3-658-26302-7.
Reachability in Binary Multithreaded Programs Is Polynomial, Alexander Malkis and Steffen Borgwardt; ICDCS 2017, Atlanta, IEEE, pp. 2083–2088. Conference participation supported by an IEEE grant.
Easy Linear Optimization, Alexander Malkis; 2016, ISBN 978-3-8440-4902-2, DOI 10.2370/9783844049022, Shaker Verlag, pp. 1–98.
Automatic Security Checks on the Model Level, Paul Muntean and Alexander Malkis; technical report TUM-I1657, 2016, Technische Universität München.
Information Exposure Checker, Paul Muntean and Alexander Malkis; technical report TUM-I1646, 2016, Technische Universität München.
A Model of Service-Oriented Architectures, Alexander Malkis and Diego Marmsoler; SBCARS'15, Belo Horizonte, © IEEE, pp. 110–119. This is the most precise, updated version. (The final publication is available from IEEE Xplore.)
Multithreaded-Cartesian Abstract Interpretation of Multithreaded Recursive Programs Is Polynomial, Alexander Malkis; RP 2015, Warsaw, Springer, pp. 114–127. Details are in the accompanying technical report [PDF] [PS]. This is the most precise, updated version. (The final publication is available at link.springer.com.)
A Model of Layered Architectures, Diego Marmsoler, Alexander Malkis, and Jonas Eckhardt; FESCA 2015, EPTCS, pp. 47–61.
On Automation in the Verification of Software Barriers: Experience Report [PDF] [PS], Alexander Malkis and Anindya Banerjee; Journal of Automated Reasoning, Volume 52, Issue 3, March 2014, Springer. This is the most precise, updated version. (The final publication is available at link.springer.com under DOI 10.1007/s10817-013-9290-9.)
The Diameter of Binary Multithreaded Programs: Preliminary Results, Alexander Malkis, Yutaka Nagashima, Steffen Borgwardt, and Claudia Eckert; research report TUM-I1361, August 2013.
On Automatic Discovery of Inductive Invariants for Parametrized Multithreaded Programs, Alexander Malkis, Corneliu Popeea, and Andrey Rybalchenko; TU München, technical report, 2012.
Verification of Software Barriers [PDF] [PS], Alexander Malkis and Anindya Banerjee; PPoPP 2012, New Orleans, ACM, pp. 313–314. The Web site contains all the details.
On the Strength of Owicki-Gries for Resources, Alexander Malkis and Laurent Mauborgne; APLAS 2011, Kenting, Springer, pp. 172–187. The technical report [PDF] [PS] contains all the proofs. This is the most precise, updated version. (The original publication is available at www.springerlink.com.)
A Practical Generic Privacy Language [PDF] [PS], Moritz Y. Becker, Alexander Malkis, and Laurent Bussard; ICISS 2010, Gandhinagar, Springer, pp. 125–139. Participation funded by IMDEA and ICISS 2010. Slides.
Thread-Modular Counterexample-Guided Abstraction Refinement [PDF] [PS] , Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko; SAS 2010, Perpignan, Springer, pp. 356–372. This is the most precise, updated version. (The original publication is available at www.springerlink.com.)
Cartesian Abstraction and Verification of Multithreaded Programs [PDF] [PS], PhD thesis, University of Freiburg, defended in 2010. Referees: A. Podelski, E.-R. Olderog.
Refinement with Exceptions [PDF] [PS], Alexander Malkis and Andreas Podelski; technical report, University of Freiburg, 2009.
Abstract Threads [PDF] [PS], Shuvendu Lahiri, Alexander Malkis, and Shaz Qadeer; VMCAI 2010, Madrid, Springer, pp. 231–246. Its long version [PDF] [PS] contains all the proofs. Conference participation supported by a SIGPLAN PAC grant.
S4P: A Generic Language for Specifying Privacy Preferences and Policies [PDF] [PS], Moritz Y. Becker, Alexander Malkis, and Laurent Bussard; Technical report MSR-TR-2010-32, Microsoft Research.
A Framework for Privacy Preferences and Data-Handling Policies, Moritz Y. Becker, Alexander Malkis, and Laurent Bussard; Technical report MSR-TR-2009-128, Microsoft Research.
Precise Thread-Modular Verification, Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko; SAS 2007, Kongens Lyngby, Springer, pp. 218–232. A long version is available: Thread-Modular Verification with Arbitrary Precision [PDF] [PS] [DVI].
Thread-Modular Verification Is Cartesian Abstract Interpretation, Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko; ICTAC 2006, Tunis, Springer, pp. 183–197. Its long version Thread-Modular Verification and Cartesian Abstraction [DVI] [PDF] [PS] was presented at the workshop Thread Verification 2006 (TV'06, part of FLoC 2006, Seattle, archived), pp. 17–27.
Polyedges, polyominoes and the Digit game [PDF] [PS], Diploma thesis, Saarbrücken, 2004. Supervisor: Raimund Seidel.
Ещё раз о компьютеризации, А. Малкис; Энергетик, 9, 1997, ISSN 0013-7278. My first invited article. Published thanks to Адольф Ушерович Липец.

Invited talks and tutorials

Proving (Security) Properties of Multithreaded Programs. May 2016, Advances Topics on IT Security, TUM, Germany.
Verification of multithreaded shared-memory programs. CBSOFT 2015, Belo Horizonte, Brazil.
Modular Verification of Multithreaded Shared-Memory Programs. September 2011, Prometidos-CM summer school, Madrid, Spain.
Verification of Shared-Memory Multithreaded Programs. December 2010, ICISS 2010, Gandhinagar, Gujarat, India.
Precise Thread-Modular Verification. July 2008, LAA 2008, Edinburgh, UK.

Development

Improvements to the Jahob verification system specific to multithreaded programs.
AMTV: Automated Modular Thread Verifier. Checks safety of multithreaded programs. Licence: GPL v3.
XAHA for Boogie: eXperimental Automatic History Abstraction. Bounded safety verifier for multithreaded programs written in Boogie.
C2PVS. A translator from C0, which is a clean subset of C, into a syntax tree in the language of the prototype verification system PVS.
The Digit game. A human-computer turn-based logical game.
Co-production of PBlast, a 3-D multiplayer shooting game for a network.

Contributed integer sequences

A096267, A097472, A290642 in the Online Encyclopedia of Integer Sequences.

Community service

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'10, ESOP'11, FM'11, SOFSEM'11, CAV'11, VMCAI'11, ICALP'12, VMCAI'12, POST'12, FACS'12, POPL'13, SOCP, ICSEA'14, CONCUR'14, Acta Informatica, FMSD, ….
PC member: VSTTE 2018.
TeX Ryge Termes Math, v. 1.548, an improved clone of TeX Gyre Termes Math, v. 1.543.

My PGP public key

Fingerprint: FBFD 76E8 D606 2B52 E9CA 954E A5B7 7667 12D2 C31B.

Jun 2017,	ICDCS'17, Atlanta, USA,	Reachability in Binary Multithreaded Programs Is Polynomial
Nov 2016,	SiBase@TUM, Munich, Germany,	Dynamic Symbolic Execution and Interpolation (talk and poster presentation)
Sep 2015,	RP'15, Warsaw, Poland,	Multithreaded-Cartesian Abstract Interpretation of Multithreaded Recursive Programs Is Polynomial
Jun 2012,	SNSF, Bern, Switzerland,	Ensuring Reliability of Parallel Software
Feb 2012,	PPoPP'12, New Orleans, USA,	Verification of Software Barriers (poster)
Nov 2011,	Z3 SIG, Cambridge University, UK,	Automatic Verification of Software Barriers: Z3 vs. MONA vs. BAPA.
Jan 2011,	EPFL, Lausanne, Switzerland,	Counterexample-Guided Thread-Modular Verification
Dec 2010,	ICISS'10, Gandhinagar, Gujarat, India,	A Practical Generic Privacy Language
Sep 2010,	SAS'10, Perpignan, France,	Counterexample-Guided Thread-Modular Verification
Jun 2010,	IMDEA, Madrid, Spain,	Cartesian Abstraction and Verification of Multithreaded Programs
Mar 2010,	IMDEA, Madrid, Spain,	Verification of Multithreaded Programs
Jan 2010,	VMCAI'10, Madrid, Spain,	Abstract Threads
Dec 2009,	UPMARC, Uppsala, Sweden,	Owicki-Gries, Thread-Modular-Reasoning, Cartesian Abstraction
Oct 2009,	ARM, Cambridge, UK,	Verification of Multithreaded Programs
Oct 2009,	Cambridge University, UK,	Owicki-Gries, Thread-Modular-Reasoning, Cartesian Abstraction
Oct 2009,	Cambridge University, UK,	Abstract Threads
Jun 2009,	MSR Cambridge, UK,	SecPAL4Privacy
Feb 2009,	EPFL, Lausanne, Switzerland,	Counterexample-Guided Thread-Modular Verification
Sep 2008,	Freiburg University, Germany,	Cartesian Abstraction Refinement
Jul 2008,	Logic and Algorithms, ICMS, Edinburgh, UK,	Cartesian Abstraction Refinement
Jul 2008,	MSR Redmond, USA,	Concurrent Histories
May 2008,	MSR Redmond, USA,	Cartesian Abstraction Refinement
Aug 2007,	SAS'07, Kongens Lyngby, Denmark,	Precise Thread-Modular Verification
Mar 2007,	EPFL, Lausanne, Switzerland,	Precise Thread-Modular Verification
Nov 2006,	ICTAC'06, Tunis, Tunisia,	Thread-Modular Verification is Cartesian Abstract Interpretation
Aug 2006,	TV'06, Seattle, USA,	Thread-Modular Verification and Cartesian Abstraction
May 2005,	MPII, Saarbrücken, Germany,	Verification of Parallel Processes (poster)