Abhinandan Pal

2 accepted papers

2025

Let a Neural Network be Your Invariant

Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, Michael Tautschnig

NeurIPS 2025poster

Safety verification ensures that a system avoids undesired behaviour. Liveness complements safety, ensuring that the system also achieves its desired objectives. A complete specification of functional correctness must combine both safety and liveness. Proving with mathematical certainty that a sy…

Cited by 6 Source ↗Scholar ↗

2024

Neural Model Checking

Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, Michael Tautschnig

NeurIPS 2024poster

We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution of a given system satisfies a desired temporal logic specification. Unlike testing, model checking provides form…

Cited by 3 Source ↗PDF ↗code ↗Scholar ↗