Program Day 2 - Wednesday 15/11/2017



09:00 - 10:00 Keynote: Self-Certifying and Secure Compilation
Kedar Namjoshi, Bell Labs, Nokia
Session chair: Itai Segall

10:00 - 11:30 Technical session: Synthesis
Session chair: Orna Grumberg

A Supervisory Control Algorithm Based on Property-Directed Reachability,
Koen Claessen, Jonatan Kilhamn, Laura Kovacs and Bengt Lennartson

SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems,
Fedor Shmarov, Nicola Paoletti, Ezio Bartocci, Shan Lin, Scott Smolka and Paolo Zuliani

A Symbolic Approach to Safety LTL Synthesis,
Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu and Moshe Y. Vardi

11:30 - 11:45 Coffee Break

11:45 - 12:45 HVC Award Ceremony and Presentation
Cristian Cadar, Imperial College London

Dynamic Symbolic Execution: Perspective and Reflections
Abstract: Dynamic symbolic execution is an effective program analysis technique that can automatically explore paths through a program. It has recently gathered significant attention, with successful application in several areas, including software testing, software engineering, computer security, program verification and software systems, among others. In this award talk, I will give my perspective on the main developments in dynamic symbolic execution and the ongoing challenges it faces.
Bio: Cristian Cadar is a Reader (Associate Professor) in the Department of Computing at Imperial College London, where he leads the Software Reliability Group. His research interests span the areas of software engineering, computer systems and security, with an emphasis on building practical techniques and tools for improving the reliability and security of software systems. He was awarded the HVC Award in 2017, a Fellowship of the British Computer Society in 2016, the ACM Computer and Communications Security (CCS) Test of Time Award in 2016, the EuroSys Jochen Liedtke Young Researcher Award in 2015, an EPSRC Early-Career Fellowship in 2013, and artifact or paper awards at ICST 2016, ISSTA 2014, ESEC/FSE 2013 and OSDI 2008. Cristian received a PhD in Computer Science from Stanford University, and undergraduate and Master's degrees from the Massachusetts Institute of Technology.
Session chair: Ofer Strichman

12:45 - 13:45 Invited Industry Talk - An Industrial Strategy for Quantum Computing, Yehuda Naveh, IBM Research
Session chair: Moshe Levinger

13:45 - 15:00 Lunch

15:00 - 16:00 Keynote: Static analysis at speed and scale
Prof. Dino Distefano, Queen Mary, University of London
Session chair: Eran Yahav

16:00 - 17:30 Technical session: SAT/SMT and Deductive Verification
Session chair: Alexander Ivrii

An Interaction Concept for Program Verification Systems with Explicit Proof Object,
Bernhard Beckert, Sarah Grebing and Mattias Ulbrich

PRuning Through Satisfaction,
Marijn Heule, Benjamin Kiesl, Martina Seidl and Armin Biere

LRA Interpolants from No Man’s Land,
Leonardo Alt, Antti Hyvärinen and Natasha Sharygina

%%sidebarspace%%
See us on Linked In See us on Facebook IBM Research Cadence Mellanox Mentor Graphics Qualcomm SunDisk