About

I’m a software engineer and researcher currently working at Amazon Web Services in the Automated Reasoning Group. My research interests include program analysis and automated reasoning at scale.

Before joining AWS, I was a postdoctoral researcher at Carnegie Mellon University researching for the Integrated Symbolic Execution for Space-Time Analysis of Code (ISSTAC) project, funded by DARPA STAC. I also worked on a NASA project on safety analysis of flight critical systems.

During my Ph.D., I worked on temporal verification of real-time embedded systems using static analysis and Timed Automata model checking using the UPPAAL model checker.

Outside of work, I enjoy running, photography and reading. Feel free to connect with me on Strava.

Publications

I currently have 32 peer-reviewed papers. I will try to keep the following list of publications up to date. You can also have a look at my Google Scholar profile and DBLP record. The copies that can be obtained here are preprints since the copyrights to many of the papers are held by the publishers.

2020

  1. Luckow, K., Kersten, R., & Pasareanu, C. (2020). Complexity vulnerability analysis using symbolic execution. Software Testing, Verification and Reliability. [BibTeX]
  2. Backes, J., Berrueco, U., Bray, T., Brim, D., Cook, B., Gacek, A., … Viswanathan, D. (2020). Stratified Abstraction of Access Control Policies. In S. K. Lahiri & C. Wang (Eds.), Computer Aided Verification (pp. 165–176). Cham: Springer International Publishing. [PDF] [BibTeX]

2019

  1. Backes, J., Bolignano, P., Cook, B., Gacek, A., Luckow, K. S., Rungta, N., … Whalen, M. (2019). One-Click Formal Methods. IEEE Software, 36(6). [PDF] [BibTeX]
  2. Păsăreanu, C. S., Kersten, R., Luckow, K., & Phan, Q.-S. (2019). Symbolic Execution and Recent Applications to Worst-Case Execution, Load Testing, and Security Analysis. [BibTeX]

2018

  1. Luckow, K., Păsăreanu, C. S., & Visser, W. (2018). Monte Carlo Tree Search for Finding Costly Paths in Programs. In Software Engineering and Formal Methods. [BibTeX]
  2. Balasubramanian, D., Kostyuchenko, D., Luckow, K., Kersten, R., & Karsai, G. (2018). A Cloud-Based Execution Framework for Program Analysis. In Software Engineering and Formal Methods. [BibTeX]
  3. Dimjašević, M., Howar, F., Luckow, K., & Rakamarić, Z. (2018). Study of Integrating Random and Symbolic Testing for Object-Oriented Software. In Integrated Formal Methods. [BibTeX]
  4. Malacaria, P., Khouzani, M., Pasareanu, C. S., Phan, Q., & Luckow, K. (2018). Symbolic Side-Channel Analysis for Probabilistic Programs. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). [BibTeX]
  5. Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., … Varming, C. (2018). Semantic-based Automated Reasoning for AWS Access Policies using SMT. In 2018 Formal Methods in Computer Aided Design (FMCAD). [PDF] [BibTeX]

2017

  1. Luckow, K., Kersten, R., & Păsăreanu, C. (2017). Symbolic Complexity Analysis Using Context-Preserving Histories. In 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST). [PDF] [BibTeX]
  2. Ravn, A. P., Thomsen, B., Søe Luckow, K., Leth, L., & Bøgholm, T. (2017). Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking. In Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. [BibTeX]
  3. Mues, M., Howar, F., Luckow, K., Kahsai, T., & Rakamarić, Z. (2017). Releasing the PSYCO: Using Symbolic Search in Interface Generation for Java. SIGSOFT Softw. Eng. Notes. [PDF] [BibTeX]
  4. Fromherz, A., Luckow, K. S., & Păsăreanu, C. S. (2017). Symbolic Arrays in Symbolic PathFinder. SIGSOFT Softw. Eng. Notes. [PDF] [BibTeX]
  5. Kersten, R., Luckow, K., & Păsăreanu, C. S. (2017). POSTER: AFL-based Fuzzing for Java with Kelinci. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. [BibTeX]

2016

  1. Luckow, K., Dimjašević, M., Giannakopoulou, D., Howar, F., Isberner, M., Kahsai, T., … Raman, V. (2016). JDart: A Dynamic Symbolic Analysis Framework. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). [PDF] [BibTeX]
  2. Luckow, K. S., & Pasareanu, C. S. (2016). Log2model: inferring behavioral models from log data. In IEEE International High Level Design Validation and Test Workshop, HLDVT 2016, Santa Cruz, CA, USA, October 7-8, 2016. [PDF] [BibTeX]
  3. Morris, R., Pasareanu, C., Luckow, K., Malik, W., Ma, H., Kumar, S., & Koenig, S. (2016). Planning, scheduling and monitoring for airport surface operations. In AAAI-16 Workshop on Planning for Hybrid Systems. [PDF] [BibTeX]
  4. Luckow, K. S., Thomsen, B., & Korsholm, S. E. (2016). HVMTP: A time predictable and portable java virtual machine for hard real-time embedded systems. Concurrency and Computation: Practice and Experience. [PDF] [BibTeX]
  5. Zhou, C., Luckow, K. S., Howar, F., & Rakamarić, Z. (2016). Visualization Support for JDart. JPF Workshop (Extended Abstract—Not in Proc.). [PDF] [BibTeX]

2015

  1. Luckow, K. S., Pasareanu, C. S., & Thomsen, B. (2015). Symbolic execution and timed automata model checking for timing analysis of Java real-time systems. EURASIP J. Emb. Sys. [PDF] [BibTeX]
  2. Thomsen, B., Luckow, K. S., Leth, L., & Bøgholm, T. (2015). From safety critical java programs to timed process models. In Programming Languages with Applications to Biology and Security. [PDF] [BibTeX]
  3. Thomsen, B., Luckow, K. S., Bøgholm, T., Thomsen, L. L., & Korsholm, S. (2015). Safety Critical Java for Robotics Programming. In Proceedings of the 3rd Aau Workshop on Robotics. [PDF] [BibTeX]

2014

  1. Luckow, K. S., & Pasareanu, C. S. (2014). Symbolic PathFinder v7. ACM SIGSOFT Software Engineering Notes. [PDF] [BibTeX]
  2. Luckow, K. S., Pasareanu, C. S., Dwyer, M. B., Filieri, A., & Visser, W. (2014). Exact and approximate probabilistic symbolic execution for nondeterministic programs. In ACM/IEEE International Conference on Automated Software Engineering, ASE ’14, Vasteras, Sweden - September 15 - 19, 2014. [PDF] [BibTeX]
  3. Luckow, K. S., Thomsen, B., & Korsholm, S. E. (2014). HVMTP: A Time Predictable and Portable Java Virtual Machine for Hard Real-Time Embedded Systems. In Proceedings of the 12th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES 2014, Niagara Falls, NY, USA, October 13-14, 2014. [PDF] [BibTeX]
  4. Luckow, K. S. (2014). Platforms and Model-based Analyses for Real-time Java: PhD Thesis. Department of Computer Science, The Faculties of Engineering, Science, and Medicine, Aalborg University. [BibTeX]

2013

  1. Bøgholm, T., Frost, C., Hansen, R. R., Jensen, C. S., Luckow, K. S., Ravn, A. P., … Thomsen, B. (2013). Towards harnessing theories through tool support for hard real-time Java programming. ISSE. [PDF] [BibTeX]
  2. Luckow, K. S., Bøgholm, T., Thomsen, B., & Larsen, K. G. (2013). TetaSARTS: a tool for modular timing analysis of safety critical Java systems. In The 11th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES ’13, Karlsruhe, Germany, October 9-11, 2013. [PDF] [BibTeX]
  3. Luckow, K. S., Bøgholm, T., & Thomsen, B. (2013). Supporting Development of Energy-Optimised Java Real-Time Systems using TetaSARTS. In WiP Proceedings of the 19th Real-Time and Embedded Technology and Application Symposium. [PDF] [BibTeX]

2011

  1. Frost, C., Jensen, C. S., Luckow, K. S., & Thomsen, B. (2011). WCET analysis of Java bytecode featuring common execution environments. In The 9th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES ’11, York, United Kingdom, September 26-28, 2011. [PDF] [BibTeX]
  2. Frost, C., Jensen, C. S., Luckow, K. S., Thomsen, B., & Hansen, R. (2011). Bluetooth Indoor Positioning System Using Fingerprinting. In Mobile Lightweight Wireless Systems - Third International ICST Conference, MOBILIGHT 2011, Bilbao, Spain, May 9-10, 2011, Revised Selected Papers. [PDF] [BibTeX]
  3. Luckow, K. S., Korsholm, S. E., & Thomsen, B. (2011). Towards a Real-Time, WCET Analysable JVM Running in 256 kB of Flash Memory. In Proceedings of the 23rd Nordic Workshop on Programming Theory. [PDF] [BibTeX]

Timeline

  • Oct 2017 - Today

    Software Development Engineer, Amazon Web Services

  • Nov 2014 - Oct 2017

    Postdoctoral Researcher, Carnegie Mellon University

  • Sept 2013 - Feb 2014

    Visiting Researcher, NASA Ames Research Center

  • Sept 2011 - Oct 2014

    Ph.D. Student, Aalborg University

  • Sept 2009 - Jun 2011

    M.Sc. Cum Laude Software Engineering, Aalborg University

  • Sept 2006 - Jun 2009

    B.Sc. Software Engineering, Aalborg University

Contact

Drop me an email if you have any questions!