Write a Blog >>
Thu 21 Jan 2016 15:10 - 15:35 at Grand Bay North - Track 1: Learning and verification Chair(s): David Monniaux

Inductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations, classified as positive, negative, and implications. We propose the first learning algorithms in this model with implication counterexamples that are based on machine learning techniques. We implement the learners and an appropriate teacher, and show that the resulting invariant synthesis is efficient and convergent for a large suite of programs.

Thu 21 Jan

POPL-2016-papers
14:20 - 16:00: Research Papers - Track 1: Learning and verification at Grand Bay North
Chair(s): David MonniauxCNRS, VERIMAG
POPL-2016-papers14:20 - 14:45
Talk
Damien OcteauUniversity of Wisconsin and Pennsylvania State University, Somesh JhaUniversity of Wisconsin, Madison, Matthew DeringPennsylvania State University, Patrick McDanielPennsylvania State University, Alexandre BartelTechnical University Darmstadt, Hongyu LiRice University, Jacques KleinUniversity of Luxembourg, Yves Le TraonUniversity of Luxembourg
Media Attached
POPL-2016-papers14:45 - 15:10
Talk
Radu GrigoreUniversity of Oxford, Hongseok YangUniversity of Oxford, UK
Media Attached
POPL-2016-papers15:10 - 15:35
Talk
Pranav GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Dan RothUniversity of Illinois at Urbana-Champaign
Media Attached
POPL-2016-papers15:35 - 16:00
Talk
Michael EmmiIMDEA Software Institute, Constantin EneaLIAFA, Université Paris Diderot
Media Attached