Here is another one of those multi-topic summaries: Dipping my toes into autonomous robot verification As I discussed here, I am exploring working with Kerstin Eder et al. (of Bristol U) regarding autonomous robot verification. So I started looking into this. I will not take you into the gory details, gentle reader (especially since I … More Misc stuff: Robotics, system simulations, AI
I attended HVC’2015 last week. Here is a partial, very subjective trip report. HVC’2015 was good. I attended the tutorial day and the first two conference days, though I was absent from most of the hard-core formal-verification sessions. Here are the main things I learned: The Bristol folks Kerstin Eder, Dejanira Araiza-Illan and David Western … More HVC’2015 trip report
Summary: This post investigates the (slightly crazy) idea of creating “one universal verification framework for everything”, and claims that while the goal itself is probably impossible (for now), some interesting and worthwhile sub-goals are perhaps possible. As many people (including myself) have discussed before, there is no single “verification community”: there are really many verification … More Is a Universal Verification Framework possible?
This is another one of those posts devoted to misc. things which may be of interest to readers of this blog. HVC The Haifa Verification Conference 2015 is upon us (Nov 16-19). If you are in Israel at that time and have nothing better to do, here are some reasons you might want to come … More Misc. stuff: HVC, game design languages and more
Summary: This post will dig into the verification challenges of autonomous systems, and especially into the challenge of verifying those which use machine learning. This post will discuss the verification of Intelligent Autonomous Systems (IAS) which have to interact with people and the outside world. Examples are AVs, UAVs, and autonomous robots of various kinds. … More Verification challenges of autonomous systems
Summary: This post explains why security research is relevant for this blog, and discusses three specific areas worth tracking. Hi folks – I’m back (vacations and all that). Security people deal with finding security issues (vulnerabilities) in systems. This blog deals with a different topic: big-system verification, where verification is defined as finding functional / … More Security research is pretty relevant for us
“Misc. stuff” posts will appear periodically. They will contain, well, miscellaneous [1] stuff – mainly links to papers and discussions which might be interesting to readers of this blog. For each, I’ll try to explain why it is relevant [2]. Hacker News and this blog My spec bugs post made it to the first page … More Misc. stuff – HN, machine learning and Jupyter
Summary: this post discusses the fact that different groups use different verification terminologies, explains why this is a problem, and suggests a common terminology page. One problem with verification is that it consists of multiple “verification tribes” or v-tribes, with different terminology and habits. There is the HW v-tribe, which I am coming from: We … More Terminology for multiple verification tribes
In a previous post I discussed verification vs. validation, and claimed that: This is a valuable distinction for a specific subsystem, but (in any complex system) this is a subsystem-relative concept, not an absolute one (as in “one man’s ceiling is another man’s floor”). I was reminded by some readers that this view (“real systems … More The soup of systems
Most bugs which kill people (and projects) are spec / requirements bugs, not implementation bugs. This could be a missing top-level requirement, a missing implication of some requirement on a lower-level spec, or some emergent behavior which was never spec’d. This post will explore the problem of spec bugs, and discuss possible solutions. Note that … More It’s the spec bugs that kill you