Summary: This post describes some new attempts at formal verification of complex systems (mainly AVs and ML-based systems) In general, I think Formal Verification (FV) will only have a limited role in verifying Intelligent Autonomous Systems (IAS) and ML-based systems, because those systems are so complex and heterogenous. In FV has better PR than CDV … More Formal verification of really-complex systems
Summary: The interactions between Autonomous Vehicles and people can be complex, which complicates AV deployment. This post summarizes some recent related publications, and then tries to predict the verification implications of all that. For instance, it suggests that verification teams will try to track total-accidents, AV-specific-accidents and AV-specific-annoyances. There were several interesting publications lately about “bumps on … More Verifying interactions between AVs and people
Summary: This post discusses the annoying “Synthetic Sensor Input” (SSI) problem, i.e. the fact that it is very hard to synthesize realistic, synchronized streams of sensor inputs (e.g. Video+LiDAR+Radar). It explains why the SSI problem is a pain for Autonomous Vehicles verification (and for other things), and talks about the (imperfect) solutions. Let me start … More The “Synthetic Sensor Input” problem in AV verification
Summary: This post tries to explain (once and for all?) how the concept of coverage is used to optimize the verification process, what it means to auto-maximize coverage, and how people have tried to do it. I have been spending some time lately on coverage maximization via ML (which I described here). As is often … More Verification, coverage and maximization: The big picture
I attended HVC again this year (see also my HVC’2015 trip report). Here is a very subjective description of what I saw and heard – much of it outside the conference room itself. Note that while HVC is about “all things verification”, much of the audience comes from the chip verification world. Also, the conference … More HVC’2016 trip report
This post covers recent updates in machine learning, autonomous systems and verification. It has four sections: Automation / ML keep accelerating, but verification of automation / ML seems to lag behind HVC is coming, and I plan to attend (and even present) The idea of training an ML-based system using synthetic inputs (which I like) … More Misc stuff: The verification gap, ML training and more
Summary: This post will take an initial look at the US Autonomous Vehicles policy announcement, and claim it is a big deal. It will then examine the verification implications, and claim they are mainly positive. Yesterday, the US Department of Transportation (DOT) and the National Highway Traffic Safety Administration (NHTSA) came out with an announcement … More Verification implications of the new US AV policy
Summary: Can one use ML to verify ML-based systems? This post claims the answer is mostly “no”: You mainly have to use other system verification methodologies. However, some ML-based techniques may still be quite useful. How does one verify ML-based systems? A previous post in this series claimed that the “right” way is CDV: Essentially, … More Using Machine Learning to verify Machine Learning?
Summary: This post describes in general terms the problem of “using ML for coverage maximization”, explains why it is important for CDV and for fuzzing, and gives some references. My first post in the “ML and verification” series talked about verifying ML-based systems (lots more to say about that). This post talks about the other … More Machine Learning for Coverage Maximization
Summary: This post – part of a series about Machine Learning (ML) and verification – discusses the hard problem of verifying ML-based systems, and how “Explainable AI” might help. I can think of three interesting topics whose title contains both “ML” and “verification”: Verifying ML-based systems Using a verification infrastructure to train ML-based systems Using … More Machine Learning verification and Explainable AI
