Closing Remarks
summary
Proposes combining partial order reduction with parameterized verification by using cesan abstraction to summarize unmodeled threads, and studies whether to apply reduction before or after abstraction; reports empirical nondeterminism in the ticket algorithm where proofs hold for two–four threads but break at five. Describes extracting formal properties from Bosch and Mercedes natural-language specs to build monitors and test generators, and pushes for producing concrete termination witnesses that other tools can validate.
AI-written summary · about
chapters (15)
- 0:00Closing remarks
- 0:48Thanks to organizers
- 1:54Retirement plans
- 2:37Software model checking
- 4:01Nondeterminism in concurrency
- 5:08Partial order reduction
- 6:35Abstraction and reduction orders
- 6:56Importance of requirements
- 8:19Natural language to formal
- 9:47Correctness requirements
- 10:09Tribute to mentors
- 11:57Answering audience questions
- 12:19Termination verification
- 13:23Cross-tool validation
- 13:44Meaning of life
related talks
58mA New Perspective on Commutativity in Verification
15mProducts of Recursive Programs for Hypersafety Verification
27mCompiling higher-order specifications to SMT solvers: how to deal with rejection ...
27mTaming Unsoundness with Gradual Abstract Interpretation
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
46mMechanizing Abstract Interpretation
18mDeveloping a Dependently Typed Language with Runtime Proof Search
23mProductivity Verification for Functional Programs by Reduction to Termination Ve...