How can a programmer ensure a critical piece of software is bug-free? Theoretical computer scientists use a fundamental question called the reachability problem, which determines whether a computer will reach or avoid various dangerous states when running a program. To better understand the complexity of the problem, researchers turned to a mathematical tool called vector addition systems. In a series of recent breakthroughs, computer scientists have now determined that the complexity of the reachability problem for vector addition systems is defined by a famous function called the Ackermann function, which becomes extremely complex even with small inputs.
----------
Read the full article for links to papers: https://www.quantamagazine.org/an-easy-sounding-problem-yields-numbers-too-big-for-our-universe-20231204/
----------
Chapters:
00:00 How Formal Verification finds programming bugs
00:59 The Reachability Problem
01:41 Origins of concurrent computing and challenges
02:40 Vector addition systems (vass) and the reachability problem
04:16 Searching for the complexity of the problem, what's the fastest algorithm?
04:38 Identification of lower and upper bounds of the problem
06:18 The Ackermann function explained
07:32 A final solution to the vas reachability problem is found
----------
- VISIT our website: https://www.quantamagazine.org
- LIKE us on Facebook: https://www.facebook.com/QuantaNews
- FOLLOW us Twitter: https://twitter.com/QuantaMagazine
Quanta Magazine is an editorially independent publication supported by the Simons Foundation: https://www.simonsfoundation.org/