Program Verification and Synthesis Techniques for Advanced Computer Science Course CS703

CS 703 Program Verification and Synthesis Fall 2023 Loris D Antoni Reps Tom

CS 703: Program Verification and Synthesis lorisdanto/cs703-program-synthesis/wiki/Schedule

CS 703: Program Verification and Synthesis Formal methods for program verification. Model-checking techniques; linear temporal logic; computational tree logic; logic/automata connection; bisimulations; probabilistic model-checking. Special topics include: program synthesis, verification and synthesis of privacy properties. Knowledge of programming languages and compiler design strongly encouraged, such as COMP SCI 536. Somesh Jha

Harvard AM 110: Spring 1974 I will only do CS703 if I can find a ``hook that will keep me excited about the material Professor A left for Silicon Valley Professor B took over AM 110 Lisp 1.5 (4 weeks) PDP-10 assembly (5 weeks) 2 assignments to modify a Lisp 1.5 interpreter written in PDP-10 assembly Not a good experience; I got the feeling that Professor B was not excited about the material

Rice COMP 607: Seminar on Computer-Aided Verification Moshe Vardi https://www.cs.rice.edu/~vardi/comp607/ https://www.cs.rice.edu/~vardi/comp607/2004/ https://www.cs.rice.edu/~vardi/comp607/2004/reviews.pdf https://www.cs.rice.edu/~vardi/comp607/2006/ https://www.cs.rice.edu/~vardi/comp607/2006/reviews06.pdf https://www.cs.rice.edu/~vardi/comp607/2008/ https://www.cs.rice.edu/~vardi/comp607/2008/reviews.pdf

The Hook Thanks to Aug. 2014 Dagstuhl Seminar Decision Procedures and Abstract Interpretation

The Hook Thanks to Aug. 2014 Dagstuhl Seminar Seshia s thesis: everything is synthesis Sanjit Seshia

Example Verification Problem Transition System Init: I x = 1 y = 1 Transition Relation: , which is repeated indefinitely x = x+y y = y+x Property: = G (y 1) Attempt to Prove by Induction: y 1 x = x+y y = y+x Fails. Need to Strengthen Invariant: Find s.t. x 1 y 1 x = x+y y = y+x Safety Verification Invariant Synthesis y 1 x 1 y 1 8

One Reduction from Verification to Synthesis NOTATION Transition system M = (I, ) Safety property = G( ) VERIFICATION PROBLEM Does M satisfy ? SYNTHESIS PROBLEM Synthesize s.t. I 9

Two Reductions from Verification to Synthesis NOTATION Transition system M = (I, ), S = set of states Safety property = G( ) VERIFICATION PROBLEM Does M satisfy ? SYNTHESIS PROBLEM #2 Synthesize : S where (M) = (I, ) s.t. (M) satisfies iff M satisfies SYNTHESIS PROBLEM #1 Synthesize s.t. I 10

The Hook Thanks to Aug. 2014 Dagstuhl Seminar Seshia s thesis: everything is synthesis The Cousots thesis: everything is abstract interpretation Mitchell s thesis: everything is learning Patrick Cousot Radhia Cousot Sanjit Seshia Tom Mitchell

Everything is Learning The set of reachable states is uncomputable Bad States Reachable States Universe of States 12

A restricted space of values. Everything is Abstract Interpretation In learning: inductive bias Finding an appropriate new abstract domain is a synthesis problem Overapproximate the reachable states via values in an abstract domain. Deliberately lose information Bad States Reachable States False positive! Universe of States 13

Everything is Abstract Interpretation Bad States Reachable States Universe of States 14

This Class: https://pages.cs.wisc.edu/~cs703-1/ Topics logic verification SAT solving abstract interpretation static-analysis path problems program synthesis including algorithms relevant to those topics Other topics semantics type theory some material related to and relevant for machine learning With each topic, some theory + some operational methods The promise: mathematical proof of, e.g., safety

The Promise: Mathematical Proof of Program Properties Difficulties and some dirty little secrets The environment Above : the surroundings (physical environment or client) Below : library methods or system calls Sensors: measurements with errors Round-off error Concurrency: huge state-space resulting from action interleavings

What About LLMs? Use an LLM to generate candidates; then symbolic methods to confirm or refute Chain of reasoning prompts? Still need verification Maybe LLM produces code + proof; verification by proof checking A proof checker is an utterly trivial program to check successors follow from predecessors Minimized the trusted computing base (idea from proof-carrying code)

This Class: https://pages.cs.wisc.edu/~cs703-1/ Topics logic verification SAT solving abstract interpretation static-analysis path problems program synthesis including algorithms relevant to those topics Other topics semantics type theory some material related to and relevant for machine learning

The Hook Program Synthesis Inductive Bias Logic Semantics Abstract Interpretation Learning &

Swan Song The swan song (Ancient Greek: ; Latin: carmen cygni) is a metaphorical phrase for a final gesture, effort, or performance given just before death or retirement. The phrase refers to an ancient belief that swans sing a beautiful song just before their death since they have been silent (or alternatively not so musical) for most of their lifetime. The belief, whose basis has been long debated, had become proverbial in ancient Greece by the 3rd century BC and was reiterated many times in later Western poetry and art. https://en.wikipedia.org/wiki/Swan_song