Markus Schordan


Email: schordan1@llnl.gov
Phone: +19254221612


Markus Schordan joined the Center for Applied Scientific Computing (CASC) in April 2013 as a senior computer scientist. His research interests include program analysis and formal software verification, reversible computation, and compiler construction. He is co-author of the software verification tool CodeThorn, the tool Backstroke for reversible computation, and the ROSE compiler infrastructure.

He previously held positions at University Klagenfurt (1997-2001), Lawrence Livermore National Laboratory (2001-2003 (Post-Doc)), TU Vienna (2003-2008), and UAS Technikum Wien 2008-2013. In 2009 he received an R&D 100 AWARD (ROSE), in 2011 a Best Paper Award at the 11th IEEE Source-Code and Manipulation Conference (SCAM 2011), and in 2012 and 2013 the Method Combination Award in the RERS Challenges (overall 3rd and 2nd respectively). In 2014 he won the RERS Challenge in 5 of 7 categories (including overall), in 2015  he won in all white box categories, and in 2017 he won with his team the RERS score-based ranking track on Linear Temporal Logic verification of sequential programs.

He received a Diploma Degree in computer science from TU Vienna in 1997, and a Ph.D. degree from University Klagernfurt in 2001 (with distinction). He is author or co-author of 35+ peer-reviewed publications. He is a member of the IFIP Working group 2.4 Software Technology, the ACM, and IEEE. He has served as co-organizer of the ISoLA 2016 track "Evaluation and Reproducibility of Program Analysis and Verification", the ISoLA 2014 track "Evaluation and Reproducibility of Program Analysis", the workshops GPUScA 2011 and GPUScA 2010, the Dagstuhl Seminar No. 08161, and the ISoLA'08 Track: Formal Methods for Analysing and Verifying Very Large Systems, and the EuroPar'03 Topic 04: Compilers for High-Performance. He served as program committee member of several conferences, most recently SOFSEM 2018, ISoLA 2016, RC 2016, Euro-Par 2015, SYNASC 2015, SOFSEM 2015, ISoLA 2014, SYNASC 2014, SYNASC 2013, ARW 2013, SYNASC 2012, GPGPU-5 2012, GPUScA 2011, CC 2011, PPPJ 2011, GPUScA 2010, SYNASC 2010, SYNASC 2009, PACT 2009, SYNASC 2008, ISoLA 2008.

Public Software Projects

  • ROSE, CodeThorn: http://www.rosecompiler.org/
  • Backstroke: https://github.com/LLNL/backstroke
  • DataRaceBench: https://github.com/LLNL/dataracebench

Awards and Achievements

  • 2017: Winner of RERS Challenge Track Sequential LTL Verification. Winner of the score-based ranking track on the verification of linear temporal logic (LTL) specifications of sequential programs. Our submitted verification results of verified reachability and linear temporal logic (LTL) properties were 100% correct (as also in 2014,2015,2016). We also got most Gold Achievements overall of all participating teams. The RERS Challenge 2017 was co-located with ISSTA and SPIN 2017. Results: http://www.rers-challenge.org/2017/index.php?page=results
  • 2015: Winner of RERS Challenge 2015. Winner in all RERS White Box Categories in 2015. We finished first in the achievement-based ranking as well as in the score-based ranking. The RERS Challenge 2015 was held as part of the 15th International Conference on Runtime Verification, September 22 - September 25, 2015 Vienna, Austria. Our submitted verification results of verified reachability and linear temporal logic (LTL) properties were 100% correct (as in 2014). The size of the verified programs was in the range of 1,420 LOC to 813,647 LOC. Results: http://www.rers-challenge.org/2015/index.php?page=results
  • 2014: Winner of RERS Challenge 2014 (category overall). Also winner in categories Plain, Arith, and Array and of the "Method Combination Prize" for winning in the category "Employed Combination of Methods". The RERS Challenge 2014 was held as a satellite event of the 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, October 8-11, 2014. The reward was a 4x200+1x100=900 EUR Springer gift certificate. Our submitted challenge analysis results of verified reachability and LTL (linear temporal logic) properties were computed using our tool CodeThorn.
    Results: http://rers-challenge.org/2014Isola/index.php?page=results#
  • 2013: "Method Combination Award " in the category "Employed Combination of Methods" in the RERS Challenge 2013 (Analysis of Event-Condition-Action Systems) Co-located with ASE 2013, Silicon Valley, California, USA, November 11 -15, 2013. The reward was a 250 EUR Springer gift certificate. Our submitted challenge analysis results were computed using our tool CodeThorn.
  • 2012: "Method Combination Prize" for winning in the category "Employed Combination of Methods" in the RERS Grey Box Challenge 2012 (Analysis of Event-Condition-Action Systems) at 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, October 15-18, 2012. The reward was a 500 EUR Springer gift certificate. Our submitted challenge analysis results were computed using our tool CodeThorn.
  • 2011: Best Paper Award SCAM 2011:
    Computation of alias sets from shape graphs for comparison of shape analysis precision.
    Viktor Pavlu, Markus Schordan, and Andreas Krall
    In Proceedings of the 11th International Working Conference on Source Code Analysis and Manipulation (SCAM 2011), IEEE, September 25-26, 2011.
  • 2009: R&D 100 Award 2009 for the project ``ROSE - Making Compiler Technology Accessible to all Programmers''. ROSE is a project at Lawrence Livermore National Laboratory (CA, U.S.A.) where I was post-doc 2001-2003 and continued to contribute to date. The official ceremony took place November 12, 2009, Orlando Florida, USA.

 

Memberships

  • IFIP Working group 2.4 Software Technology (full voting member)

  • ACM and IEEE

 

Organizing Committees

Chair

 

Editor of Proceedings and Journal Issues

  • Eduard Mehofer, Markus Schordan, Dan Quinlan, and Beniamino Di Martino (Editors). Special Issue on GPUs and Scientific Applications. International Journal of Computational Science and Engineering.
  • Beniamino Di Martino, Eduard Mehofer, Dan Quinlan, and Markus Schordan (Editors). Special Issue on Graphical Processing Units and Scientific Applications. International Journal High Performance Computing Applications, 26(3):189--191, August 2012.
  • Eduard Mehofer, Markus Schordan, Dan Quinlan, and Beniamino Di Martino (Editors). Proceedings of the 2nd International Workshop on GPUs and Scientific Applications, 51 pages, Galveston Island, Texas, USA, October 10, 2011. Proceedings available as technical report. Department of Scientific Computing, University of Vienna.
  • Eduard Mehofer, Markus Schordan, Dan Quinlan, and Beniamino Di Martino (Editors). Proceedings of the 1st International Workshop on GPUs and Scientific Applications, 65 pages, Vienna, Austria, September 11, 2010. Proceedings available as technical report. Department of Scientific Computing, University of Vienna.

 

My Publications

My page in the DBPL Computer Science bibliography (Markus Schordan)

My page at Google Scholar (Markus Schordan)

 

Journal Publications

  • Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. Markus Schordan and Adrian Prantl. International Journal on Software Tools for Technology Transfer (STTT), Volume 16, Issue 5 (2014), Pages 493-505, 2014.
  • Computation of alias sets from shape graphs for comparison of shape analysis precision. Viktor Pavlu, Markus Schordan, Andreas Krall. IET Software, Volume 8 (2014), Issue 3, pp. 120-133, 2014.
  • Comparison of type-based and alias-based component recognition for embedded systems software. Dietmar Schreiner, Gergo Barany, Markus Schordan, and Jens Knoop. International Journal on Software Tools for Technology Transfer (STTT), DOI: 10.1007/s10009-012-0251-0, 2012.
  • Beyond Loop Bounds: Comparing Annotation Languages for Worst-Case Execution Time Analysis. Raimund Kirner, Jens Knoop, Adrian Prantl, Markus Schordan, and Albrecht Kadlec. Journal of Software and System Modelling, pages 1--27, Springer (online edition), ISSN: 1619-1366, 2010.
  • The Language of the Visitor Design Pattern. Markus Schordan. Journal of Universal Computer Science (JUCS), Vol. 12, No. 7, pp. 849-867, August 2006. Special Issue: Selected Papers from The 10th Brazilian Symposium on Programming Languages. Issue edited by Mariza Andrade Silva Bigonha and Alex de Vasconcellos Garcia
  • Parallel Object-Oriented Framework Optimization. Daniel Quinlan, Markus Schordan, Brian Miller, and Markus Kowarschik. Concurrency and Computation: Practice and Experience. Volume 16, Issue 2-3 , pp. 293-302. Special Issue: Compilers for Parallel Computers. Issue Edited by Michael O'Boyle.
    Copyright © 2004 John Wiley & Sons, Ltd.

 

Selected Conference Publications

Verifying the Floating-Point Computation Equivalence of Manually and Automatically Differentiated Code
Markus Schordan, Jan Huckelheim, Pei-Hung Lin, Harshitha Menon. Verifying the Floating-Point Computation Correctness'17: First International Workshop on Software Correctness for HPC Applications, in conjunction with SC17: The International Conference for High Performance Computing, Networking, Storage and Analysis, November 12, 2017, Denver, Colorado, USA. In cooperation with SIGHPC, accepted.

DataRaceBench: A Benchmark Suite for Systematic Evaluation of Data Race Detection Tools
(nominated for best paper)

Chunhua Liao, Pei-Hung Lin, Joshua Asplund, Markus Schordan, Ian Karlin.
Supercomputing 2017: The International Conference for High Performance Computing, Networking, Storage and Analysis, Nov 12-17, 2017, Denver, Colorado, USA, to appear.

The RERS 2017 Challenge and Workshop (Invited Paper)
Marc Jasper, Maximilian Fecke, Bernhard Steffen, Markus Schordan, Jeroen Meijer, Jaco van de Pol, Falk Howar,Stephen F. Siegel. International SPIN Symposium on Model Checking of Software, July 2017, Santa Barbara, CA, USA, to appear.

Dealing with Reversibility of Shared Libraries in PDES
Davide Cingolani, Alessandro Pellegrini, Markus Schordan, Francesco Quaglia, David R. Jefferson. Proceedings of the 2017 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, SIGSIM-PADS 2017, Singapore, May 24-26, 2017. ACM 2017, ISBN 978-1-4503-4489-0.

Multi-core Model Checking of Large-scale Reactive Systems Using Different State Representations.
Marc Jasper and Markus Schordan. In Tiziana Margaria and Bernhard Steffen,
editors, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece,
October 10-14, 2016, Proceedings, Part I, volume 9952 of Lecture Notes in Computer
Science, pages 212–226. Springer International Publishing, 2016.

Automatic generation of reversible C++ code and its performance in a scalable kinetic monte-carlo application.
Markus Schordan, Tomas Oppelstrup, David Jefferson, Peter D. Barnes Jr., and Daniel J.Quinlan. In Richard Fujimoto, Brian W. Unger, and Christopher D.
Carothers, editors, Proceedings of the 2016 annual ACM Conference on SIGSIM Principles of Advanced Discrete Simulation, SIGSIM-PADS 2016, Banff, Alberta, Canada, May
15-18, 2016, pages 111–122. ACM, 2016.

RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification.
Maren Geske, Marc Jasper, Bernhard Steffen, Falk Howar, Markus Schordan, and Jaco
van de Pol. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of
Formal Methods, Verification and Validation: Discussion, Dissemination, Applications 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016,
Proceedings, Part II, volume 9953 of Lecture Notes in Computer Science, pages 787–803.
Springer International Publishing, 2016.

Evaluation and Reproducibility of Program Analysis and Verification (Track Introduction).
Markus Schordan, Dirk Beyer, and Jonas Lundberg. In Tiziana Margaria and Bernhard
Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation:
Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu,
Greece, October 10-14, 2016, Proceedings, Part I, volume 9952 of Lecture Notes in Computer Science, pages 191–194. Springer International Publishing, 2016.

Reverse Code Generation for Parallel Discrete Event Simulation.
Markus Schordan, David Jefferson, Peter Barnes, Tomas Oppelstrup, Daniel Quinlan. In Proceedings of the 7th Conference on Reversible Computation. Jean Krivine and Jean-Bernard Stefani (Eds.): Reversible Computation, LNCS 9138, pp. 95-110, ISBN 978-3-319-20859-6, Springer, 2015.

Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations.
Markus Schordan, Pei-Hung Lin, Dan Quinlan, and Louis-Noel Pouchet. In Proceedings of the 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation.  T. Margaria and B. Steffen (Eds.): ISoLA 2014, Part II, LNCS 8803, pp. 493--508. Springer, Heidelberg (2014).

Computation of Alias Sets from Ahape Graphs for Comparison of Shape Analysis Precision.
Viktor Pavlu, Markus Schordan, and Andreas Krall. In Proceedings of the 11th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2011), IEEE, September 25-26, 2011. [Best Paper Award SCAM 2011]

From Trusted Annotations to Verified Knowledge
Adrian Prantl, Jens Knoop, Raimund Kirner, Markus Schordan, and Albrecht Kadlec
In Post-Workshop Proceedings of the 9th International Workshop on Worst-Case Execution Time Analysis (WCET 2009), Dublin, Ireland, Austrian Computer Society, Volume 252, ISBN 978-3-85403-252-6, pp. 39 - 49, 2009.

Adding Timing-Awareness to AUTOSAR Basic-Software - A Component Based Approach
Dietmar Schreiner, Markus Schordan, and Jens Knoop
In Proceedings of the 12th IEEE International Symposium on Object/component/service-oriented Real-time distributed Computing (ISORC 2009), Tokyo, Japan, ISBN 978-0-7695-3573-9, pp. 288 - 292, March 17-20, 2009.

Component Based Middleware-Synthesis for AUTOSAR Basic Software
Dietmar Schreiner, Markus Schordan, Karl M. Göschka
Proceedings of the '12th IEEE International Symposium on Object/component/service-oriented Real-time distributed Computing (ISORC09)', Tokyo, Japan, ISBN 978-0-7695-3573-9, March 17-20, 2009.

Constraint Solving for High-Level WCET Analysis
Adrian Prantl, Jens Knoop, Markus Schordan, Markus Triska
In Proceedings of the 18th Workshop on Logic-based Methods in Programming Environments (WLPE 2008), pp. 77-88, Udine, Italy, December 12, 2008.

ALL-TIMES - a European Project on Integrating Timing Technology
Jan Gustafsson, Björn Lisper, Markus Schordan, Christian Ferdinand, Marek Jersak, Guillem Bernat
In Proceedings of the 3rd International Symposium on Leveraging Applications of Formal Methods (ISOLA'08), pp. 445-459, Springer, Porto Sani, Greece, Editors: Tiziana Margaria and Bernhard Steffen.

TuBound - A Conceptually New Tool for Worst-Case Execution Time Analysis
Adrian Prantl, Markus Schordan, Jens Knoop
In Post-Workshop Proceedings of the 8th International Workshop on Worst-Case Execution Time Analysis (WCET 2008), Austrian Computer Society, Volume 237, ISBN 978-3-85403-237-3, pp. 141 - 148, Prague, Czech Republic, July 1, 2008.

WCET Analysis: The Annotation Language Challenge
Raimund Kirner, Jens Knoop, Adrian Prantl, Markus Schordan, Ingomar Wenzel
7th Workshop on WCET Analysis, Pisa, Italy, July 3, 2007.
In Post-Workshop Proceedings of the 7th   International Workshop on Worst-Case Execution Time   Analysis (WCET 2007), pp. 83-99, 2007.

Classification and Utilization of Abstractions for Optimization
Daniel Quinlan, Markus Schordan, Qing Yi, and Andreas Saebjornsen
Leveraging Applications of Formal Methods, First International Symposium , ISoLA 2004, Paphos, Cyprus, October 30 - November2, 2004, Revised Selected Papers (ISoLA'04)
Lecture Notes in Computer Science, Volume 4313, pp. 57-73, Springer Verlag, ISSN 0302-9743, ISBN 978-3-540-48928-3, November 02, 2006.

The Language of the Visitor Design Pattern
Markus Schordan
10th Brazilian Symposium on Programming Languages (SBLP'06)
Itatiaia, Rio de Janeiro, Brazil, May 2006.
Proceedings of the 10th Brazilian Symposium on Programming Languages, pp. 235-248, ISBN 85-7669-071-3, ANAIS, May 2006.

Annotating User-Defined Abstractions for Optimization
Daniel Quinlan, Markus Schordan, Richard Vuduc, and Qing Yi
Workshop on Performance Optimization for High-Level Languages and Libraries (POHLL'06) in conjunction with 20th IEEE International Parallel & Distributed Processing Symposium (IPDPS 2006)
Rhodes Island, Greece, April 2006.
Proceedings of the 20th IEEE International Parallel & Distributed Processing Symposium (IPDPS 2006), Workshop on Performance Optimization for High-Level Languages and Libraries, CDROM, IEEE Computer Society, 2006.

Specifying Transformation Sequences as Computation on Program Fragments with an Abstract Attribute Grammar
Markus Schordan and Daniel Quinlan
Fifth IEEE International Workshop on Source Code Analysis and Manipulation (SCAM'05)
Budapest, Hungary, September 2005.
Proceedings of the Fifth IEEE International Workshop on Source Code Analysis and Manipulation, pp. 97-106, IEEE, ISBN 0-7695-2292-0, 2005.

Toward the Automated Generation of Components from Existing Source Code
Daniel Quinlan, Qing Yi, Gary Kumfert, Thomas Epperly, and Tamara Dahlgren, Markus Schordan, and Brian White
2nd Workshop on Productivity and Performance in High-End Computing (P-PHEC)
San Francisco, CA, U.S.A, February 2005.
Proceedings of the 2nd Workshop on Productivity and Performance in High-End Computing, pp. 12-19, 2005.

Classification and Utilization of Abstractions for Optimization
Daniel Quinlan, Markus Schordan, Qing Yi, and Andreas Saebjornsen
1st International Symposium on Leveraging Applications of Formal Methods (ISoLA'04)
Preliminary Proceedings, pp. 2-9, TR-2004-6, Department of Computer Science, University Cyprus, October 2004.

Semantic-Driven Parallelization of Loops Operating on User-Defined Containers
Daniel Quinlan, Markus Schordan, Qing Yi, and Bronis de Supinski
16th Annual Workshop on Languages and Compilers for Parallel Computing (LCPC'03), College Station, TX, USA, October 2-4, 2003. Revised Papers.
Lecture Notes in Computer Science, vol. 2958, pp. 524-538, Springer Verlag, May 2004

A Source-To-Source Architecture for User-Defined Optimizations
Markus Schordan and Daniel Quinlan
Joint Modular Languages Conference (JMLC'03)
Lecture Notes in Computer Science, vol. 2789, pp. 214-223, ISBN 978-3-540-40796-6, Springer Verlag, August 2003.

A C++ Infrastructure for Automatic Introduction and Translation of OpenMP Directives
Daniel Quinlan, Markus Schordan, Qing Yi, and Bronis de Supinski
Workshop on OpenMP Applications and Tools (WOMPAT'03)
Lecture Notes in Computer Science, vol. 2716, pp. 13-25, Springer Verlag, June 2003.

Treating a User-Defined Parallel Library as a Domain-Specific Language
Daniel Quinlan, Brian Miller, Bobby Philip, and Markus Schordan
7th International Workshop on High-Level Parallel Programming Models and Supportive Environments (HIPS'02)
In Proceedings of the 16th International Parallel and Distributed Processing Symposium
Ft. Lauderdale, USA, pp. 105-114, IEEE Press, April 2002.

The Specification of Source-To-Source Transformations for the Compile-Time Optimization of Parallel Object-Oriented Scientific Applications
Dan Quinlan, Markus Schordan, Bobby Philip, and Markus Kowarschik
In Proceedings of the 14th International Workshop on Languages and Compilers for Parallel Computing (LCPC'01)
Lecture Notes in Computer Science, vol. 2624, pp. 570-578, Springer Verlag, August 2001.

Virtual Method Resolution with Typed Alias Graphs
Markus Schordan and Wolfram Amme
In Proceedings of the 8th International Workshop on Compilers for Parallel Computers (CPC'00)
Aussois, France, pp. 151-162, January 2000.

PAOLA-Program Analysis of Object-Oriented Languages
Wolfram Amme, Markus Schordan, Wilhelm Rossak, and Laszlo Boeszoermenyi
International Workshop on Aliasing in Object-Oriented Systems (IWAOOS'99)
In European Conference on Object-Oriented Programming (ECOOP'99) Workshop Reader, Lisbon, Portugal,
Lecture Notes in Computer Science, vol. 1743, pp. 143-146, Springer Verlag, June 1999.

JavaSet: extending Java by persistent sets
Markus Schordan, Harald Kosch, and Laszlo Boeszoermenyi
In Proceedings of the 3rd International Austrian-Israeli Technion Symposium, Software for Communication Technologies'99,
pp. 58-66, Hagenberg, Linz, Austria, April 1999.