Pavol Černý
Professor
Forsyte group,
Faculty of Informatics,
TU Wien
Curriculum vitæ
Email:
pavol.cerny@tuwien.ac.at
Office: HC 03 11
Professor
Forsyte group,
Faculty of Informatics,
TU Wien
Curriculum vitæ
Email: pavol.cerny@tuwien.ac.at
Office: HC 03 11
Forsyte group,
Faculty of Informatics,
TU Wien
Curriculum vitæ
Email: pavol.cerny@tuwien.ac.at
Office: HC 03 11
Welcome!
- My research area is computer-aided verification, and I focus on program synthesis. I have recently worked on applications in networking, artificial intelligence, and software engineering.
- I am fortunate to work with a great group of PhD students. I am looking for postdocs and PhD students who are enthusiastic about verification and logic.
- I teach undergraduate courses on (concurrent) programming and graduate courses on computer-aided verification and program synthesis.
News
- I will move to TU Wien in September 2019, and join the Forsyte group at the Faculty of Informatics. I am looking forward to the new position, and I am extraordinarily grateful for the six happy years at CU Boulder.
- Efficient Detection and Quantification of Timing Leaks with Neural Networks accepted to RV 2019.
- Sequential Programming for Replicated Data Stores accepted to ICFP 2019.
- Quantitative Mitigation of Timing Side Channels accepted to CAV 2019.
- Type-directed Bounding of Collections in Reactive Programs accepted to VMCAI 2019.
- Congratulations to Jed McClurg who will join University of New Mexico as an Assistant Professor in Fall 2018.
- Congratulations to Saeid Tizpaz Niari for his ECEE departmental Gold Student Research Award for 2017/2018.
- DroidStar: Callback Typestates for Android Classes accepted to ICSE 2018.
- Differential Performance Debugging with Discriminant Regression Trees accepted to AAAI 2018.
Current Students
- Tianhan Lu (PhD, co-advised with Evan Chang, since 2015)
- Saeid Tizpaz Niari (PhD, since 2015)
- Nicholas Lewchenko (PhD, since 2016)
Alumni
PhD
- Jedidiah McClurg. PhD, 2018. First employment: Assistant professor, CS, University of New Mexico.
MS
- Nilesh Jagnik. MS, 2016. First employment: Google.
Independent study
- Parker Evans. (Undergraduate) Discovery Learning Apprenticeship, 2013-14.
- Prabhash Krishnan (2015-16), Aniket Lata (2015-16), Krishna Sripada (2015-16), Vaibhav Singh (2014-15). Graduate Independent Study.
- Andrew Dudney (Fall 2016). Undergraduate Independent Study.
Student awards
- Saeid Tizpaz Niari. ECEE Departmental Outstanding Gold Research Award. 2018.
- Jedidiah McClurg. Computer Science Departmental Outstanding Research Award. 2017.
- Saeid Tizpaz Niari. Second prize, Microsoft Research Open Source Challenge. 2016.
Open positions
We are looking for enthusiastic PhD students and postdocs to join CUPLV. Please send me an email if you are interested in research on program verification and program synthesis.
Current Projects
Program synthesis for networks
ML+PL for performance and security
Learning typestates
Past Projects
Streaming transducers
Streaming string transducers [POPL11] are as appealing a model for regular string transformations as deterministic finite automata are for regular languages. The transformations definable by streaming string transducers are exactly those that are definable by classical two-way transducers and monadic second-order logic [FSTTCS10].
Simulation distances
Standard verification tools return a yes/no answer that indicates whether a system satisfies its specification. However, not all correct implementations are equally good, and not all incorrect implementations are equally bad. Simulation distances [CONCUR10,EMSOFT12,GandALF12] capture a finer and more quantitative view of the relationship between specifications and systems.
Quantitative abstraction refinement
To enable efficient static analysis of programs for estimating the value of a quantitative property such as worst-case execution time, we need to abstract the program. We have proposed an abstract interpretation technique to reason about quantitative properties [POPL13], and applied it to worst-case execution time analysis [ESOP15].
Synchronization synthesis
Our program synthesis techniques for concurrency [CAV13,CAV14,CAV15b] allow programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a standard, more aggressive, preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior.
Software model checking for confidentiality
Courses at CU Boulder
- ECEN 1310: Programming for Engineers. Spring 2019.
- ECEN 5139, CSCI 5135: Computer-Aided Verification. Fall 2018.
- ECEN 1310: Programming for Engineers. Spring 2018.
- ECEN 5139, CSCI 5135: Computer-Aided Verification. Fall 2017.
- ECEN 4313, CSCI 4830: Concurrent Programming. Spring 2017.
- ECEN 5033, CSCI 7000-005: Program Synthesis. Fall 2016.
- ECEN 4003, CSCI 4830: Concurrent Programming. Spring 2016.
- ECEN 5033, CSCI 7000-005: Program Synthesis. Fall 2015.
- ECEN 4003, CSCI 4830: Concurrent Programming. Spring 2015.
- ECEN 5139, CSCI 5135: Computer-Aided Verification. Fall 2014.
- ECEN 5033, CSCI 7000-007: Concurrent Programming. Spring 2014.
- ECEN 5139, CSCI 5135: Computer-Aided Verification. Fall 2013.
- ECEN 5033, CSCI 7000-007: Program Synthesis. Spring 2013.
Previous Courses
- Programming Paradigms for Concurrency. Co-instructor, Fall 2010, IST Austria and TU Wien.
- CIS 399: C++ programming. Instructor, Spring 2009, University of Pennsylvania.
- CSE 399: C/C++ programming. Co-instructor, Spring 2006, University of Pennsylvania.
- CIS 511: Theory of Computation. TA, Spring 2005, University of Pennsylvania.
- CSE 482: Logic in Computer Science. TA, Fall 2004, University of Pennsylvania.
Program committees
- CAV 2020, PC member
- VMCAI 2020, PC member
- CAV 2019, PC member
- SYNT 2019, workshop PC member
- ATVA 2018, PC member
- CAV 2018, PC member
- POPL 2018, PC member
- CAV 2016, PC member
- EC2 2016, workshop PC chair
- TACAS 2016, PC member
- POPL 2016, ERC member
- GandALF 2015, PC member
- SYNT 2015, workshop PC chair
- EC2 2015, PC member
- PLVNET 2015, workshop PC chair
- CAV 2014, PC member
- EMSOFT 2014, PC member
- SYNT 2014, workshop PC member
- MEMICS 2011, workshop PC member
Publications (DBLP, Google Scholar)
Selective conferences
- Efficient Detection and Quantification of Timing Leaks with Neural Networks. New!
- Sequential Programming for Replicated Data Stores. New!
- Quantitative Mitigation of Timing Side Channels. New!
- Type-directed Bounding of Collections in Reactive Programs. New!
-
DroidStar: callback typestates for Android classes.
New!Arjun Radhakrishna, Nicholas V. Lewchenko, Shawn Meier, Sergio Mover, Krishna Chaitanya Sripada, Damien Zufferey, Bor-Yuh Evan Chang, Pavol Černý.
ICSE, 2018.
[pdf] - Differential Performance Debugging with Discriminant Regression Trees. New!
- Synchronization Synthesis for Network Programs.
- Discriminating Traces with Time. Saeid Tizpaz-Niari, Pavol Černý, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, Ashutosh Trivedi.
TACAS, 2017.
[pdf] - Optimizing Horn Solvers for Network Repair.
- Optimal Consistent Network Updates in Polynomial Time.
- Event-driven network programming.
- Synthesis Through Unification.
- From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis. Pavol Černý, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach.
CAV, 2015.
[pdf] - Segment Abstraction for Worst-Case Execution Time Analysis. Pavol Černý, Thomas A. Henzinger, Laura Kovács, Arjun Radhakrishna, Jakob Zwirchmayr.
ESOP, 2015.
[pdf] - Efficient synthesis of network updates.
- Regression-Free Synthesis for Concurrency. Pavol Černý, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach.
CAV, 2014.
[pdf] - Efficient Synthesis for Concurrency by Semantics-Preserving Transformations. Pavol Černý, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach.
CAV, 2013.
[pdf] - Quantitative abstraction refinement.
- Synthesis from incompatible specifications. Pavol Černý, Sivakanth Gopi, Thomas A. Henzinger, Arjun Radhakrishna, Nishant Totla.
EMSOFT, 2012.
[pdf] - Interface Simulation Distances
- Quantitative Synthesis for Concurrent Programs. Pavol Černý, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, Rohit Singh.
CAV, 2011.
[pdf] - The Complexity of Quantitative Information Flow Problems.
- Streaming transducers for algorithmic verification of single-pass list-processing programs.
- Model Checking of Linearizability of Concurrent List Implementations.
- Simulation Distances.
- Automated Analysis of Java Methods for Confidentiality.
- Algorithmic Analysis of Array-Accessing Programs.
- Parallel programming with object assemblies.
- Model Checking on Trees with Path Equivalences.
- Preserving Secrecy Under Refinement.
- Synthesis of interface specifications for Java classes.
Journals
-
From non-preemptive to preemptive scheduling using synchronization synthesis.
Pavol Černý, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach.
Formal Methods in System Design 50: 97-139 (2017).
[pdf] - Interface simulation distances. Pavol Černý, Martin Chmelik, Thomas A. Henzinger, Arjun Radhakrishna.
Theor. Comput. Sci. 560: 348-363 (2014).
[pdf] - Simulation distances.
- Algorithmic analysis of array-accessing programs.
Invited contributions
- From boolean to quantitative synthesis.
- Quantitative Simulation Games.
- Expressiveness of streaming string transducers.
Workshops with proceedings
- Performance search engine driven by prior knowledge of optimization.
- Toward Synthesis of Network Updates.
- Security Evaluation of ES&S Voting Machines and Election Management System. Adam J. Aviv, Pavol Černý, Sandy Clark, Eric Cronin, Gaurav Shah, Micah Sherr, Matt Blaze.
EVT, 2008.
[pdf]
Theses
- Software Model Checking for Confidentiality.
- Verification by Abstract Interpretation of Parameterized
Predicates.
Report
- EVEREST: Evaluation and Validation of Election-Related
Standards and Testing.