Notes from CAV 2022
Notes from attending FLoC 2022 as a student volunteer at Haifa, Israel. There is no notes after the third day due to a combination of jet lag, exhaustion, and mild sickness.
Neural Network Verification
Shared Certificates for Neural Network Verification

Even two input spaces (perturbation on a single input) can be very different, at later hidden layer the transformed output spaces may still contain each other.
 Classification output partition is very coarse comparing with input space.

Check subset relation between transformed output spaces at any hidden layer

Template is a set in a hidden layer that potentially is a super set of some input spaces after transformation. and the output space of template satisfies the robustness spec.
 Heuristic to choose templates.

Improve efficiency for nn verification
Example Guided Synthesis of Linear Approximations for Neural Network Verification

Compute linear overapproximations for different nonlinear neuron activation functions (e.g., sigmoid)

Accumulate overapproximations becomes overly conservative

Minimize volume between linear overapproximation and true function

Offline synthesis (need to understand details)

upshift to address violation to address unsound linear approximations
 violation is a point of true function larger/above than the line defining approximations.
 find upper bound on the violation using nonlinear optimization encoding the true function.
Trainify: A CEGARDriven Training and Verification Framework for Verifiable Deep Reinforcement Learning

partition the continuous state space to finite abstract states and train neural network on abstract states as input
 Seems to be a straightforward partition (grid based)

Convert system with NN to Kripke structure
 Construct an explicit state transition system
 Get action from nn using an abstract state as input and calculate next abstract state by evaluating concrete state evolution
 Property directed reduction/simplification on abstract transition systems
 Need more detail?

Verify against ACTL (temporal logic) using existing tools

Refinement process?
 This might be the most interesting part?

Small examples with nn controllers
Affine Loop Invariant Generation via Matrix Algebra
 Infer loop invariants for piecewise affine transition functions as the loop body

Encode proof of inductive step into checking Farka’s lemma holds
 (exists linear combination of guard and inv on prestate x) /\ loop body => the guard and inv on poststate x’
 “exists linear combination of guard and inv on prestate x” is a nonlinear constraints

Two methods to synthesize invariants based on eigenvalue and matrix inverse
 Looks simple enough to understand
 Applications in finding our AAPs?
Datadriven Numerical Invariant Synthesis with Automatic Generation of Attributes

discover attributes (feature variables) instead of enumerate all
 Use convex shapes as “separator”
 Learn disjunction of convex constraints
 “Joinmax” separator

What is the maximal guarantee for the synthesized invariants?
Logic Lounge: Autonomous systems
ResponsibilitySensitive Safety (RSS) analysis for multiagent (related to Sungwoo’s work)

Driving Policy
 Assume
 “Safetynet”
 Proper response within unsafe states (safe but close to bad states)
 Guarantee
 If all agents apply proper response, collision avoidance is still guaranteed under unsafe states
 Duty of care  legal obligation
 Safetyusefulness tradeoff
Aug. 8, Monday
 Koopman operator linearization
 https://github.com/EthanJamesLew/AutoKoopman
 STLmc
 Model checking for Signal Temporal Logic over what?
 Robustness check
 Is it able to model stability, ISS, ultimately bounded property
 Barrier certificates
 UCLID5
 SyGus with Oracle? Synthesize contract for perception/state estimation functions.

add assumption over input output pairs
 f(x) = y, positive sample
 f(x) != y, negative sample
 I(x) ==> I(x’), inductive example
 Satisfiability algorithm
 Synthesis algorithm?
CAV award 2022
 Determinism
 Time and function are (reasonably) independent
Real time with stream input
 Software level “Virtually Synchronous”
 Timed Triggered Architecture~(TTA)  single rate [HK et al 90]
 Proven correct in PVS
 Physically asynchronous Logically synchronous~(PALS) [JM et al 09]
 Lingua Franca~(LF) reactor model [EL et al 2019]
 Timed Triggered Architecture~(TTA)  single rate [HK et al 90]
Problem in synchronous When deadline/delay is larger than the period (cycle time). IF we change the function to address delay, the function and time are now dependent.
Kahn Process Networks~(KPN)!!!
 Read until all inputs are ready in FIFO queue.

Asynchronous Write
 KPN is deterministic under arbitrary interleaving/fair scheduling
 independent of computation/communication delays!!!
With well typed KPN, FIFO queue for read can be bounded. Timed KPN – KPN with timed constraints Still deterministic functions rom timed input to timed output streams.
node type > a step function with input and output typed with segments of stream connector type > constraints on matching segment length from producer node to consumer node.
type checking > bounded memory and deadlock free