Let a Neural Network be Your Invariant
Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, Michael Tautschnig
Safety verification ensures that a system avoids undesired behaviour, acrucial requirement for the design of reactive systems, especially hardwaresystems.  Liveness complements safety, ensuring that the system alsoachieves its desired objectives.  A complete specification of functionalcorrectness must combine both safety and liveness aspects.  Proving withmathematical certainty that a system satisfies a safety property demandspresenting an appropriate inductive invariant of the system, whereasliveness requires showing a measure of progress also known as rankingfunctions.  Neural model checking has recently introduced a data-drivenapproach to the formal verification of reactive systems, albeit focusing onranking functions and thus addressing only liveness properties.  In thispaper, we extend and generalise neural model checking to additionallyencompass inductive invariants and thus safety properties as well.  Given asystem and a linear temporal logic specification of safety and liveness, ourapproach alternates a learning and a checking component towards theconstruction of a provably sound neural certificate.  Our new methodintroduces a neural certificate architecture that jointly representsinductive invariants as proofs of safety, and ranking functions as proofs ofliveness.  Moreover, our new architecture is able to leverage constraintsolvers for training, accelerating cognate neural model checking work otherwise basedon gradient descent.  We experimentally demonstrate that our method is several orders of magnitude faster than the state-of-the-art model checkers on pure liveness and combined safety and liveness verification tasks written in SystemVerilog, while enabling the verification of richer properties than was previously possible forneural model checking.