Assigned Readings:

I'm always tweaking the reading list, so this list will mutate over time. Also, I'm building on many old reading lists, so if you go read the commented-out HTML, you'll see old readings listed. Some of those we'll use, but some we won't. (But they're all good papers...)

Week 0:

These two papers are optional, and you haven't learned enough to understand most of the details yet (You will!), but these are nice ways to get motivated, by seeing impressive industrial case studies that show successful adoption of modern, automated, formal verification techniques. For now, just skim over anything that doesn't make sense (or google/wikipedia them if you're curious), and concentrate on the results!

• Thomas Ball, Ella Bounimova, Rahul Kumar, Vladimir Levin, "SLAM2: Static Driver Verification with under 4% False Alarms," FMCAD'10: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, ACM 2010, pp. 35-42.
• Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Panday, Anna Slobodova, Christopher Taylor, Vladimir Frolov, Erik Reeber, Armaghan Naik, "Replacing Testing with Formal Verification in Intel Core i7 Processor Execution Engine Validation", Proceedings of 21st International Conference on Computer-Aided Verification (CAV'09), Springer LNCS Vol. 5643, pp. 414-429, 2009. The paper is long and detailed, but it describes Intel's experience using formal verification instead of traditional simulation-based methods, resulting in lower cost and higher quality. Intel has been investing heavily in formal verification since the Pentium FDIV bug back in 1995.

• Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis, "Turing Lecture: Model Checking: Algorithmic Verification and Debugging", Communications of the ACM, Vol. 52, No. 11 (November 2009), pp. 74-84.
Again, a lot of it won't make sense yet, but it will! Ed's section is the broader overview, and Allen's section gives more details about temporal logic. I think if you click through to the PDF version, it will be easier to read (with all the figures in the right places).

Hey, there's video now, too!

• Here's Byron Cook's plenary talk at the Federated Logic Conference FloC 2018,

• Byron Cook, "Formal Reasoning about the Security of Amazon Web Services", 30th International Conference on Computer-Aided Verification (CAV), 2018, Springer LNCS 10980--10981.

Week 1:

Randal E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", ACM Computing Surveys, Vol. 24, No. 3 (September 1992), pp. 293-318. (Preprint published as CMU CS Tech Report CMU-CS-92-160.) Sections 1 to 3 are the relevant ones for us, although the whole paper is excellent. Here is a link to the official version at the ACM Digital Library. You have free access from UBC machines.

Karl S. Brace, Richard L. Rudell, and Randal E. Bryant, "Efficient Implementation of a BDD Package", 27th Design Automation Conference, pp. 40-45, 1990. How BDD packages are really implemented. (Optional.)

Randal Bryant, "On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Applications to Integer Multiplication", IEEE Transactions on Computers, Vol. 40, No. 2, February 1991. A general technique for proving BDDs big for certain functions (and getting better intuition about what makes BDDs big). (Optional. You may find this interesting if you like theory and/or are interested in understanding what makes BDDs blow up.) Here is additional explanation of the combinatorial part of Bryant's multiplication proof. Optional

I hope we'll have time to take a quick look at cutpoints for combinational equivalence. Here are some of the classic references on practical techniques for scaling combinational equivalence checking up to practical sizes. (These are all optional.)

• Daniel Brand, "Verification of Large Synthesized Designs", International Conference on Computer-Aided Design, pp. 534-537, 1993. This is probably the most cited paper, presenting a fully worked out version of the cutpoint idea. But, it's old and so harder to read.
• C. Leonard Berman and Louise H. Trevillyan, "Functional Comparison of Logic Designs for VLSI Circuits", International Conference on Computer-Aided Design, pp. 456-459, 1989. This is the original introduction of the cutpoint idea, but this paper is even older and harder to read.
• Andreas Kuehlmann and Florian Krohm, "Equivalence Checking Using Cuts and Heaps", 34th Design Automation Conference, pp. 263-268, 1997. This papers covers most of the tricks used in modern tools.

Week 2:

Joao Marques-Silva, Ines Lynce, and Sharad Malik, "Conflict-Driven Clause Learning for SAT Solvers", Chapter 4 in the Handbook of Satisfiability, Armin Biere, Marijhn Heule, Hans van Maaren, and Toby Walsch, Eds., IOS Press, 2008. I found this link (unofficial, but at Princeton, where Sharad is a professor) to a somewhat more updated treatment of the material, whereas I used to refer to the original papers. This looks good, and I've used in for 513 a few times. Let me know if you like this. Let me know if you like this reading.

A long time ago, I wrote up some additional explanatory notes, which I think were really excellent back in the day. I realized that they had gotten really out-of-date, though, so I was going to update them. But instead, I found these great explanatory notes on implication graphs and clause learning by Tommi Junttila. ( Optional ) (Solely for historical reference, these are my old, additional explanation notes (DEPRECATED). I recommend not reading my old notes, but am leaving the link, as I know some former students refer to my reading lists.)

Similarly, these are some classic papers on CDCL SAT solving, and are still listed here purely for reference.

• Lintao Zhang and Sharad Malik, "The Quest for Efficient Boolean Satisfiability Solvers", Invited Paper, Proceedings of 14th Conference on Computer Aided Verification (CAV2002), Copenhagen, Denmark, July 2002, Springer Lecture Notes in Computer Science Volume 2404, pp. 17-36. (Also in Proceedings of 8th International Conference on Computer Aided Deduction (CADE 2002).) Optional This is the reading that I've recommended for many years. A good survey of the big breakthrough in complete SAT solving for verification applications, about 15 years ago.
• My notes above were based in part from this additional paper: Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver", ICCAD 2001, pp. 279-285. Optional

I may move the material below later in the term, as I want to try this year to accelerate the assignments, so that you all get a wider range of exposures to different topics before embarking on a project. But these are two papers on extracting a proof out of modern SAT solver.

• Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt, Jr., "DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs", Theory and Applications of Satisfiability Testing (SAT), 2014, pp. 422-429. (Unofficial link to a copy on one of the author's (old) websites) This is a near-state-of-the-art paper on this topic. The proof generation procedure is actually easier than in the paper below, but it relies on more powerful proof steps, whereas the classic paper below uses only resolution. Optional
• Lintao Zhang and Sharad Malik, "Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications," DATE 2003, pp. 10880-10885. This is the classic paper on getting a proof out of a modern SAT solver. It's also a nice description and proof of correctness of the algorithm used in current SAT solvers. Optional

Week 3 (and Into Week 4)

OK, we're going to switch to software verification next. However, I'm going to rush through just what we need to get to SMT solving (like SAT, but with more expressive logics) and the next assignment. We'll come back later and backfill the classical basics for software verification, and maybe some interesting twists on SMT solving.

For symbolic execution:

• The classic original paper is "Symbolic Execution and Program Testing" by James King in Communications of the ACM, 19(7) (July 1976), pp. 385-394. This already has pretty much everything there. It just needed breakthroughs in SMT solving to become practical.
• Just for fun, here's an optional paper, where we see the cutpoint idea reappearing for checking equivalence of software: Xiushan Feng, and Alan J. Hu, "Cutpoints for Formal Equivalence Verification of Embedded Software", International Conference on Embedded Software (EMSOFT), 2005, pp. 307-316. Optional. (It also compares performance with a functional encoding (the way you did Assignment 1 with BDDs) vs. a relational encoding (the way you did Assignment 2 with SAT and the Tseitin transform). I'm not sure how these results would change with modern SMT solvers, though.)
• I plan to briefly introduce DART (Directed Automated Random Testing)/Concolic testing, but not sure if we'll have time now, or squeeze this later in the term. (This is sort of like a cross between fuzzing and symbolic execution.) I believe the DART paper is the original: Patrice Godefroid, Nils Klarlund, Koushik Sen, "DART: Directed Automated Random Testing", PLDI 2005, pp. 213-223. (Optional)
• Koushik went on to name this approach "concolic testing" and built on it in the open, academic literature: Koushik Sen, Darko Marinov, Gul Agha, "CUTE: A Concolic Unit Testing Engine for C", ESEC/FSE 2005, pp. 263-272. (Optional)
• Around the same timeframe, what would eventually become the KLEE project took off, based on very similar ideas: Cristian Cadar, Vijay Ganesh, Peter Pawlowski, David Dill, Dawson Engler, "EXE: Automatically Generating Inputs of Death", ACM CCS 2006, pp. 322-335. (Optional) Anecdotally, I've heard (including from my own students) positive things about building on and experimenting with the KLEE tool, so it's something to consider using for your projects/research.

My former student and SMT expert Sam Bayless recommended a great survey paper on SMT solving, by two of the very best experts out there. This is easier than the papers I used to use. Leonardo de Moura, and Nikolaj Bjorner, "Satisfiability Modulo Theories: An Appetizer," Formal Methods: Foundations and Applications -- 12th Brazilian Symposium on Formal Methods, Springer LNCS Volume 5902, 2009, pp. 23-36. SMT is basically SAT solving, but with additional logics that are very useful for software verification and other applications where you don't want to model everything as Booleans.

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio, and Roberto Sebastiani, "Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis", Annals of Mathematics and Artificial Intelligence, Vol. 55, No. 1-2, pp. 63-99. This is the paper I used to recommend, and looking at it again, it does a great job of presenting more details, although the above paper is easier to read. Check this one if you are excited and want to learn more. (Optional) (Later: I realized that my enthusiasm for Leo and Nikolai above could be interpreted as a critique of these authors, and I totally don't mean that! This survey is from another one of the top teams in SMT solving. It's extraordinarily hard to build and maintain a competitive, general-purpose SMT solver, so the research community that actually builds SMT solvers is dominated by a few small groups of rock stars.)

Greg Nelson, and Derek C. Oppen, "Simplification by Cooperating Decision Procedures," ACM Transactions on Programming Languages and Systems, 1(2), October 1979, pp. 245-257. For reference, this is a classic paper on the topic. Nelson and Oppen pioneered this area, and their work still underlies and guides a lot of research in this area. (Optional)

Week 4 (after finishing SMT) (and into Week 5)

We now shift our focus to "reactive systems", which are systems that maintain an on-going interaction with the environment (cf. "agents"). The key difference is that we now worry about how a system behaves over time, versus just checking whether a function computes the correct result.

The most basic computational tool is computing reachability, the set of states the system can get into. We'll briefly explore two basic approaches:

Explicit Reachability: The basic ideas are really simple, but you can do some interesting stuff with it. I'm not going to push the readings too hard, though. Here are some optional papers.

• David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang, "Protocol Verification as a Hardware Design Aid", International Conference on Computer Design, 1992. (non-paywalled mirror) This is a light-weight paper on the value of using very high-level formal verification to debug hardware. It also introduces the Murphi verifier, which is a nice system to play with guarded commands, non-determinism, and reachability.
• C. Norris Ip and David L. Dill, "Better Verification Through Symmetry", International Conference on Computer Hardware Description Languages, 1993. (non-paywalled mirror) This paper describes automatic symmetry reductions for explicit state enumeration -- one of the cool tricks that can greatly reduce the number of states you need to explore.
• For hash compaction as implemented in Murphi, it looks as if the definitive paper never got published. For a citable reference, try U. Stern and D. L. Dill. Improved Probabilistic Verification by Hash Compaction, Correct Hardware Design and Verification Methods: IFIP WG 10.5 Advanced Research Working Conference, CHARME '95 Springer LNCS Volume 987, 1995, pp. 206-224. For the state-of-the-art using Bloom filters, see Peter C. Dillinger and Panagiotis Manolios, Bloom Filters in Probabilistic Verification, FMCAD 2004.

Symbolic Reachability: I haven't found a description of the basic reachability computation with BDDs that fits into the course well. Accordingly, I list here three optional papers. The simplest description is one I wrote for a survey paper a million years ago. Section II.C is the relevant part. Alan J. Hu, "Formal Hardware Verification with BDDs: An Introduction", IEEE Pacific Rim Conference on Communications, Computers, and Signal Processing (PACRIM'97), 1997. This is a bit too breezy for our course. Two other possible papers are "A Unified Framework for the Formal Verification of Sequential Circuits" by Coudert and Madre, which is a dense, but good paper by two of the pioneers in this area, and "Implicit State Enumeration of Finite State Machines using BDD's [sic]" by Touati, Savoj, Lin, Brayton, and Sangiovanni-Vincentelli, which is easier to read, although I don't particularly like some of their notation. Both of these papers appeared in the International Conference on Computer-Aided Design in 1990. ( All of these papers are optional.)

Week 5

I think the preceding "week"'s reading will cover us through this week as well. As I was revising my lecture notes, I realized that I'm hoping to look at the idea of abstraction (again), but this time for reactive systems. And I'm thinking of giving an (incredibly brief, cocktail-party-level) intro to abstract interpretation as an example of reachability with conservative abstraction. And since I don't expect to revisit this topic, I should provide a (very optional) link to the classic paper that introduced abstract interpretation. (This is a tough read, but it's a classic, and one of the most cited papers in computer science.) Patrick Cousot and Radhia Cousot, "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints," Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 1977.

Week 6

We spent a bit longer on abstraction than I had planned, but that's good, as it lays the groundwork for later, as we'll encounter abstraction over and over again. Anyway, this means that we'll do symbolic reachability this week, which is incredibly cool (at least to me), and then a quick intro to temporal logic, which is the main theoretical framework for specifying more complex properties about reactive systems, beyond just reachability.

For temporal logic, Allen Emerson has written an amazing chapter in the Handbook of Theoretical Computer Science. This book is well worth buying. (2024 update: Oh my! The two volumes were expensive back when I was a young faculty member, but they are crazy expensive now!) But, a draft of the chapter is available on-line directly from Allen. This is optional. It's an encyclopedic reference.

Week 7

And now, we're ready for another Turing-Award-winning topic: model checking. For model checking (Turing Award 2007 to Ed Clarke, Allen Emerson, and Joseph Sifakis), we're going to jump straight to symbolic model checking. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, "Symbolic Model Checking: 10^{20} States and Beyond", Information and Computation, Vol. 98, No. 2, June 1992. This is the journal version of the original paper on symbolic model checking (which appeared in the Conference on Logic in Computer Science in 1990). The paper goes into more depth than what I expect of you and is rather theoretical, but I want you all to understand symbolic model checking for CTL at least. (We'll cover roughly the material from Sections 1-4 and 6 in class.)

Time-permitting, we'll look at LTL model checking, which has become increasingly fashionable (whereas I have historically emphasized CTL model checking because CTL and model checking go together so well). Given that many of you may encounter LTL in your research, we'll do a quick intro to LTL model checking. I struggled quite a bit to select readings, as there's a vast literature on this topic, some of it quite theoretical.

• Pierre Wolper, "The Tableau Method for Temporal Logic: An Overview", Logique et Analyse, Issue 110-111, Pages 119-136, 1985. The writing is a bit loose here and there, but this is the friendliest, most intuitive introduction I've seen for converting from LTL to an automaton (although it's not even phrased as such -- it's actually solving satisfiability of LTL, but it's the same underlying idea). I will base my lecture on this, and combined with the additional background I'll provide, this should be a good, basic understanding. (Optional)
• Orna Lichtenstein, and Amir Pnueli, "Checking that Finite State Concurrent Programs Satisfy Their Linear Specification", 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'85), pp. 97-107. If you want a more rigorous treatment, this is one of the classic papers. This is dense reading -- it's amazing how much stuff is packed in here! (Optional)
• Fabio Somenzi, and Roderick Bloem, "Efficient Buechi Automata from LTL Formulae", International Conference on Computer-Aided Verification (CAV 2000), pp. 248-263. This is a more modern treatment of the topic. I provide this paper for a number of reasons: the intro gives a big picture of how these LTL-to-automata techniques are used for model checking as well as good overview of a lot of the previous results, and also the tool they produced Wring is still generally useful. (Optional)

Week 8

Sorry for posting late. We did LTL model checking on Tuesday. Next, we'll move on to how to use SAT to do model checking. For Thursday, I think we'll do Bounded Model Checking (BMC), which is a really simple idea, but has had a lot of success in practice. If we have time, I might also introduce Craig interpolants. Next week (which is a short week due to the break), we'll tackle IC3, which is the state-of-the-art in SAT-based model checking (although in practice, no method completely dominates the others, so people still do use BDDs, and interpolation, often as part of a portfolio of algorithms).

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs," Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), LNCS Vol. 1579. This is the original paper on bounded model checking.

This is a good survey of the pre-IC3 approaches to using SAT for unbounded model checking: Mukul R. Prasad, Armin Biere, and Aarti Gupta, "A Survey of Recent Advances in SAT-Based Formal Verification", Software Tools for Technology Transfer, Vol 7 No 2 (April 2005), pp. 156-173. (Optional)

And Ken McMillan's original interpolation paper was a major breakthrough and is still a very insightful approach. K. L. McMillan, "Interpolation and SAT-Based Model Checking," Computer-Aided Verification: 15th International Conference (CAV'2003), LNCS Vol. 2725, Springer, 2003, pp. 1-13. (Optional)

Week 9

We only get one lecture this week, due to the mini reading break in the schedule.

I somehow always feel like I need to read at least two different papers explaining IC3 to have a feel for what's going on. Here are the core IC3 papers that I recommend. Given what I just said, perhaps the "assignment" should be to read any two of these four (the last one is for historical reference)! :-):

• Aaron R. Bradley, "SAT-Based Model Checking Without Unrolling," Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011. This paper is considered the authoritative reference for IC3. I think this paper is really the must-read if you want to understand IC3. The next two papers are friendlier, but they aren't precise enough to understand the details. You might start with those, though.
• Fabio Somenzi, and Aaron R. Bradley, "IC3: Where Monolithic and Incremental Meet", Formal Methods in Computer-Aided Design (FMCAD) 2011. This is meant as a gentle tutorial, and it includes a fully worked small example. However, I always find the small example to be too much detail, and I bog down on it.
• "Efficient Implementation of Property Directed Reachability", Formal Methods in Computer-Aided Design (FMCAD) 2011. This paper is also meant to be explanatory, as well as going into optimizations from the PDR folks. I found this easier to follow overall, but there were spots that were hard to pin down. My lecture will more closely follow the construction in this paper, so if you are reading after my lecture, you might start here.
• Aaron R. Bradley, "Understanding IC3", SAT 2012: Theory and Applications of Satisfiability Testing, 2012. Aaron is the originator of IC3, and this is a newer paper that gives history, context, and philosophy behind how he came up with the algorithm. I think this is super-interesting, but you probably need to have at least a rough feel of how the algorithm works before you can follow this one. This is a non-paywalled link to Aaron's personal archive of the paper.
• Aaron Bradley, and Zohar Manna, "Checking Safety by Inductive Generalization of Counterexamples to Induction", Formal Methods in Computer-Aided Design (FMCAD), 2007, pp. 173-180. This is the origin of the idea, but it's not the newest version of IC3. It does contain more info on clause generalization, though. It's also interesting for historical reference. (Optional)

Week 10

Funny, several years back, people voted hybrid systems off the syllabus, but this year, there's renewed interest. Many years back, I'd sometimes spend a couple weeks on this, and then later, I'd sometimes try to cram everything into a single lecture. I'm going to try this year to give you a very light introduction to the area, so that you'll have a basic feel for the area, and will be equipped to read more if you want. So, this will likely be 1-2 lectures.

For your reference, these are a great set of lecture notes to introduce continuous and hybrid systems, developed by John Lygeros of the University of Patras: John Lygeros, "Lecture Notes on Hybrid Systems", Notes for an ENSIETA short course, February 2-6, 2004. . (Optional) (This document appears to be floating around unpublished. Obviously, we don't have time to go through all of this, but these notes are provided as a background reference for you.)

New this year, I just stumbled across the draft of a book, which appears not to have ever been published. This is by John Lygeros, together with Claire Tomlin and Shankar Sastry, who are all major big shots in this area. I haven't gone through this, but it looks good. John Lygeros, Claire Tomlin, Shankar Sastry, Hybrid Systems: Modeling, Analysis and Control, December 28, 2008. (Optional)

OK, sorry for the VERY late addition, but I wanted to try to cover Reluplex this year, and I got very, very far behind on my lecture prep. Reluplex is an SMT solver optimized for neural network verification, and was the winner of this year's CAV Award. I'll be working from the arXiv version of the original CAV paper for this lecture. (Optional)

Week 11

For Tuesday, I think it's time to revisit SAT -- in particular, the problem of getting a proof out of the SAT solver when the result is UNSAT. (When the result is SAT, you can easily check the answer by plugging in the satisfying assignment.)

• Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt, Jr., "DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs", Theory and Applications of Satisfiability Testing (SAT), 2014, pp. 422-429. (Unofficial link to a copy on one of the author's (old) websites) This is a near-state-of-the-art paper on this topic. The proof generation procedure is actually easier than for resolution proofs in the Zhang and Malik paper below, but it relies on more powerful proof steps. resolution. (Optional)
• Evgueni Goldberg and Yakov Novikov, "Verification of Proofs of Unsatisfiability for CNF Formulas," DATE 2003, pp. 10886-10891. (Unofficial link to a copy on one of the author's websites) I was recently reminded that the key idea behind the above paper (actually, behind DRUP, which is the main idea behind DRAT) was actually published many years earlier, in the same conference as the resolution proof paper below. But somehow, the idea sat (no pun intended) mostly ignored until the DRAT folks built up a lot of cool machinery around it. (Optional)
• Lintao Zhang and Sharad Malik, "Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications," DATE 2003, pp. 10880-10885. This is the classic paper on getting a proof out of a modern SAT solver. It's also a nice description and proof of correctness of the algorithm used in current SAT solvers. (Optional)
• Oh, and just for fun, here is a news article describing the generation of a 200TB proof for the Boolean Pythagorean Triples problem, generated using these techniques and a SAT solver. (Optional)

For Thursday this week, we'll return to ancient history: the classic, foundational papers on formal specification and verification of software.

• C. A. R. Hoare, "An Axiomatic Basis for Computer Programming", Communications of the ACM, October 1969, pp. 576-583. This is a classic paper on the basic ideas of software verification. From UBC machines, you'll see a link for the full-text PDF.
• Edsger W. Dijkstra, "Guarded Commands, Nondeterminacy, and the Formal Derivation of Programs," Communications of the ACM, 18(8), August 1975, pp. 453-457. Another classic on the foundations of software verification. This paper introduced guarded commands and weakest precondition. From UBC machines, you'll see a link for the full-text PDF.
• R. W. Floyd, "Assigning Meanings to Programs", Proceedings of Symposia in Applied Mathematics, Vol. 19, 1967, pp. 19-32. This is the true original. Interesting -- in the past, I hadn't found an official copy on-line of this paper, but there were always a bunch of decent scanned copies available. But this year, I'm seeing only this unofficial scan, which is pretty clear, but appears a bit too zoomed in. A lot of other scans have disappeared, but Springer now seems to have an official link to a reprint of the original paper that was republished as a chapter of a book of collected papers in 1993. I'm guessing that Springer might be going around issuing take-down notices to unofficial reprints. Fortunately, you can access this via your UBC CWL. I also have an official hardcopy reprint and can make copies if anyone is interested. (Back in the old days, before the Internet or even laser printers became widespread, when you published a paper, the publisher would send you a fixed number of printed copies of your paper, called "reprints". If someone wanted a copy of your paper and didn't have access to the journal in a nearby library, they'd send you a physical mail request for a reprint, and you'd physically mail them a copy. I have an official reprint that Bob Floyd gave me, as he was cleaning out his stuff.) And, whoa... Cliff Jones has put up what appears to be a scan of the original conference handout of Floyd's paper! This definitely far surpasses my OG street cred! (The purple color indicates that these were printed in a very small batch, using a ditto machine, which is how we used to print small volumes of identical material (e.g., course handouts), back when photocopiers either didn't exist, or were prohibitively expensive.) Optional (all versions).

And... if you want to see a more modern application... some years ago, two 513 students had to miss a few lectures to attend OSDI (the flagship conference for operating systems research). At the same time that we were going over classic Floyd-Hoare software verification, the OSDI folks were getting a talk from some folks at Microsoft (with academic collaborators) on an end-to-end software verification project using Floyd-Hoare reasoning (helped by the sort of automation we've covered). It's a cool paper, and they did some really impressive stuff. At the same time, you can see the weakness of this approach, as there's still a huge amount of manual effort to add the required annotations (about 5x more annotation than code), which limits scalability and economic viability. I saw Chris give a great talk on a related project (verifying cryptographic code) last summer, and activity in this area is continuing. Chris Hawblitzel, Jon Howell, Jacob Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill, "Ironclad Apps: End-to-End Security via Automated Full-System Verification", OSDI 2014. (Optional)

Week 12

The topic for Tuesday, or maybe the whole week, is synthesis, specifically syntax-guided synthesis for programs. Sorry this is getting posted so late. I'm basically pulling an all-nighter to get this lecture(s?) together, as I haven't covered this material before, and there's a LOT of stuff. I will aim to just give you all some background and context around this, with some basic examples and intuition, to help you navigate this material and read the papers if you are interested in more. (In fact, one of the pioneers of SyGuS, Armando Solar-Lezama, has notes online for an entire course on program synthesis, if you're interested.)

For the readings, let me recommend Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukkund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa, "Syntax-Guided Synthesis", Formal Methods in Computer-Aided Design (FMCAD), 2013, which is the paper that launched the term "Syntax-Guided Synthesis". It's sort of a survey paper, written by several of the leading groups that were pioneering related approaches. I'll hopefully also get to talk about Flashfill, which is the big success for synthesis to date. The paper in CACM, Sumit Gulwani, William R. Harris, and Rishabh Singh, "Spreadsheet Data Manipulation Using Examples", Communications of the ACM, August 2012, Vol. 55, No. 8, is a combo of three prior papers. It's written to be more of an overview, although you'll need to read the linked papers for more details. (All these papers are optional.)

OK, for the last lecture of the course, we're going to talk about... concurrent software! This was quite a last-minute switch.

I had heard great things about a new parallel SAT solver, called Mallob or MallobSat , and I was thinking it'd be good to do a lecture on this. However, as I dove into the details, it didn't actually look like a good topic for a lecture in this course, as the papers are all about how they very very carefully balanced various factors and built on efficient concurrent data structures to get good parallelization of a portfolio of SAT solvers. It'd be better for a course on parallel computing, for example. Still, this is apparently the best-performing, most powerful SAT solver out there, so it's good to know about (and now you do!), if you ever have to deal with big SAT problems and have good parallel computing available.

So, what to lecture about instead? Back at the beginning of the term, I asked the various formal-related faculty if there were topics that they hoped I might cover (e.g., Ron suggested the synthesis stuff). Alex suggested that I might cover assume-guarantee reasoning for concurrent software. There's a large literature on assume-guarantee reasoning, so I kind of hesitated to try to do a quick intro, but I found a nice paper by two folks who have done a lot of influential, fairly practical work on concurrent software verification. This is a great, fairly accessible taste of this area of research: Cormac Flanagan and Shaz Qadeer, "Assume-Guarantee Model Checking", 10th SPIN Workshop (2003). Looking at that paper reminded me about later work, that also had practical impact, on context-bounded analysis of concurrent software. (Shaz, with Dinghao Wu, introduced the idea in this paper. (Optional)) Since this course is a high-level overview of lots of different things, I will link to one of my own papers, which is a quick intro to three different approaches to context bounded analysis: Naghmeh Ghafari, Alan J. Hu, Zvonimir Rakamaric, "Context-Bounded Translations for Concurrent Software: An Empirical Evaluation", 17th International SPIN Workshop on Model Checking Software (2010). (Not sure if we'll have time to get to this.)

Finally, from the Mallob folks, I found a link to an Amazon Science blog post by Byron Cook, who leads Amazon's Automated Reasoning Group. Byron has far greater social intelligence than I do (and he's no slouch in other intelligence, either!), so instead of my snarky cynicism, his blog post is a great, inspiring look forward at the increasing promise of automated verification technology. I think that's a perfect note on which to end the course.

Don't read ahead of here (unless you want to), since I haven't picked all the papers for this year yet. The "week" labels are also likely very wrong, since the course mutates a bit every year.

Week n+1:

And now, we get to symbolic model checking. There are actually two different Turing Awards discussed in this week's material.

• First, we need to introduce temporal logic (Turing Award 1996 Amir Pnueli). For temporal logic, Allen Emerson has written an amazing chapter in the Handbook of Theoretical Computer Science. This book is well worth buying. But, a draft of the chapter is available on-line directly from Allen. This is optional. It's an encyclopedic reference.
• For model checking (Turing Award 2007 to Ed Clarke, Allen Emerson, and Joseph Sifakis), we're going to jump straight to symbolic model checking. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, "Symbolic Model Checking: 10^{20} States and Beyond", Information and Computation, Vol. 98, No. 2, June 1992. ( old, non-paywalled, ps file ) This is the journal version of the original paper on symbolic model checking (which appeared in the Conference on Logic in Computer Science in 1990). The paper goes into more depth than what I expect of you and is rather theoretical, but I want you all to understand symbolic model checking for CTL at least. (We'll cover roughly the material from Sections 1-4 and 6 in class.)

Week n+2:

Last week was short due to the new mental health break in UBC's schedule, so we wrapped up symbolic model checking on Monday, and for Wednesday, we'll look at LTL model checking, which has become increasingly fashionable lately (whereas I have historically emphasized CTL model checking because CTL and model checking go together so well). Given that many of you may encounter LTL in your research, we'll do a quick intro to LTL model checking. I struggled quite a bit to select readings, as there's a vast literature on this topic, some of it quite theoretical.

• Pierre Wolper, "The Tableau Method for Temporal Logic: An Overview", Logique et Analyse, Issue 110-111, Pages 119-136, 1985. The writing is a bit loose here and there, but this is the friendliest, most intuitive introduction I've seen for converting from LTL to an automaton (although it's not even phrased as such). I will base my lecture on this, and combined with the additional background I'll provide, this should be a good, basic understanding.
• Orna Lichtenstein, and Amir Pnueli, "Checking that Finite State Concurrent Programs Satisfy Their Linear Specification", 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'85), pp. 97-107. If you want a more rigorous treatment, this is one of the classic papers. This is dense reading -- it's amazing how much stuff is packed in here! Note that this paper is paywalled, but you have free access via UBC. I haven't figured out how to give you a nice link, but if you go to the UBC Library home page , and then search for the paper (with author names and title, etc.), you can get access. (Optional)
• Fabio Somenzi, and Roderick Bloem, "Efficient Buechi Automata from LTL Formulae", International Conference on Computer-Aided Verification (CAV 2000), pp. 248-263. This is a more modern treatment of the topic. I provide this paper for a number of reasons: the intro gives a big picture of how these LTL-to-automata techniques are used for model checking as well as good overview of a lot of the previous results, and also the tool they produced Wring is still generally useful. (Optional)

Week n+3?:

Week n+4:

I somehow always feel like I need to read at least two different papers explaining IC3 to have a feel for what's going on. Here are the core IC3 papers that I recommend. Given what I just said, perhaps the "assignment" should be to read any two of these four (the last one is for historical reference)! :-):

• Aaron R. Bradley, "SAT-Based Model Checking Without Unrolling," Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011. This paper is considered the authoritative reference for IC3. I think this paper is really the must-read if you want to understand IC3. The next two papers are friendlier, but they aren't precise enough to understand the details. You might start with those, though.
• Fabio Somenzi, and Aaron R. Bradley, "IC3: Where Monolithic and Incremental Meet", Formal Methods in Computer-Aided Design (FMCAD) 2011. This is meant as a gentle tutorial, and it includes a fully worked small example. However, I always find the small example to be too much detail, and I bog down on it.
• "Efficient Implementation of Property Directed Reachability", Formal Methods in Computer-Aided Design (FMCAD) 2011. This paper is also meant to be explanatory, as well as going into optimizations from the PDR folks. I found this easier to follow overall, but there were spots that were hard to pin down. My lecture will more closely follow the construction in this paper, so if you are reading after my lecture, you might start here.
• Aaron R. Bradley, "Understanding IC3", SAT 2012: Theory and Applications of Satisfiability Testing, 2012. Aaron is the originator of IC3, and this is a newer paper that gives history, context, and philosophy behind how he came up with the algorithm. I think this is super-interesting, but you probably need to have at least a rough feel of how the algorithm works before you can follow this one. This is a non-paywalled link to Aaron's personal archive of the paper.
• Aaron Bradley, and Zohar Manna, "Checking Safety by Inductive Generalization of Counterexamples to Induction", Formal Methods in Computer-Aided Design (FMCAD), 2007, pp. 173-180. This is the origin of the idea, but it's not the newest version of IC3. It does contain more info on clause generalization, though. It's also interesting for historical reference. (Optional)

For the classical foundation on software verification:

• C. A. R. Hoare, "An Axiomatic Basis for Computer Programming", Communications of the ACM, October 1969, pp. 576-583. This is a classic paper on the basic ideas of software verification. From UBC machines, you'll see a link for the full-text PDF.
• Edsger W. Dijkstra, "Guarded Commands, Nondeterminacy, and the Formal Derivation of Programs," Communications of the ACM, 18(8), August 1975, pp. 453-457. Another classic on the foundations of software verification. This paper gets a bit ahead of ourselves, as we'll see guarded commands and non-determinism later, but this introduces weakest precondition. From UBC machines, you'll see a link for the full-text PDF.
• R. W. Floyd, "Assigning Meanings to Programs", Proceedings of Symposia in Applied Mathematics, Vol. 19, 1967, pp. 19-32. This is the true original. I can't find an official copy on-line, but there are some scanned copies on-line, e.g. here . I also have an official hardcopy reprint and can make copies if anyone is interested. (Back in the old days, before the Internet or even laser printers became widespread, when you published a paper, the publisher would send you a fixed number of printed copies of your paper, called "reprints". If someone wanted a copy of your paper and didn't have access to the journal in a nearby library, they'd send you a physical mail request for a reprint, and you'd physically mail them a copy. I have an official reprint that Bob Floyd gave me, as he was cleaning out his stuff.) Optional.

And... if you want to see something more modern... a few years ago, two 513 students had to miss a few lectures to attend OSDI (the flagship conference for operating systems research). At the same time that we were going over classic Floyd-Hoare software verification, the OSDI folks were getting a talk from some folks at Microsoft (with academic collaborators) on an end-to-end software verification project using Floyd-Hoare reasoning (helped by the sort of automation we'll get to soon). It's a cool paper, and they did some really impressive stuff. At the same time, you can see the weakness of this approach, as there's still a huge amount of manual effort to add the required annotations, which limits scalability and economic viability. I saw Chris give a great talk on a related project (verifying cryptographic code) last summer, and activity in this area is continuing. Chris Hawblitzel, Jon Howell, Jacob Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill, "Ironclad Apps: End-to-End Security via Automated Full-System Verification", OSDI 2014. (Optional)

Week 7:

LTL has become increasingly fashionable lately (whereas I have historically emphasized CTL model checking because CTL and model checking go together so well). Therefore, given that many of you may encounter LTL in your research, I figured that I really should give you all an introduction to LTL model checking. I struggled quite a bit to select readings, as there's a vast literature on this topic, some of it quite theoretical. I'm going to select just two papers for you: one to give a taste for the classical, original approach to LTL model checking; and the second to describe one of the main workhorses in practice for checking liveness properties (which tend to get emphasized more in LTL model checking, but also apply for CTL).

• Pierre Wolper, "The Tableau Method for Temporal Logic: An Overview", Logique et Analyse, Issue 110-111, Pages 119-136, 1985. The writing is a bit loose here and there, but this is the friendliest, most intuitive introduction I've seen for converting from LTL to an automaton (although it's not even phrased as such). I will base my lecture on this, and combined with the additional background I'll provide, this should be a good, basic understanding.
• Orna Lichtenstein, and Amir Pnueli, "Checking that Finite State Concurrent Programs Satisfy Their Linear Specification", 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'85), pp. 97-107. If you want a more rigorous treatment, this is one of the classic papers. This is dense reading -- it's amazing how much stuff is packed in here! Note that this paper is paywalled, but you have free access via UBC. I haven't figured out how to give you a nice link, but if you go to the UBC Library home page , and then search for the paper (with author names and title, etc.), you can get access. (Optional)
• Fabio Somenzi, and Roderick Bloem, "Efficient Buechi Automata from LTL Formulae", International Conference on Computer-Aided Verification (CAV 2000), pp. 248-263. This is a more modern treatment of the topic. I provide this paper for a number of reasons: the intro gives a big picture of how these LTL-to-automata techniques are used for model checking as well as good overview of a lot of the previous results, and also the tool they produced Wring is still generally useful. (Optional)
• Armin Biere, Cyrille Artho, Viktor Schuppan, "Liveness Checking as Safety Checking", 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'02), Electronic Notes in Theoretical Computer Science 66 No. 2 (2002). This is my other "assigned" paper for this week. As mentioned, this is one of the main workhorse methods in practice for dealing with liveness properties, so it's good to know about.
• Naghmeh Ghafari, Alan J. Hu, Zvonimir Rakamaric, "Context-Bounded Translations for Concurrent Software: An Empirical Evaluation", International SPIN Workshop on Model Checking Software (SPIN 2010), LNCS Vol. 6349, pp. 227-244.
  Akash Lal, Thomas Reps, "Reducting Concurrent Analysis Under a Context Bound to Sequential Analysis", International Conference on Computer-Aided Verification (CAV 2008), LNCS Vol 5123, pp. 37-51.
  This is a topic jump, if we get to it, based on the underlying theme (and a really powerful idea) that if we're doing formal verification, we can make non-deterministic guesses in our solution, and trust the verification process to find the correct guess if one exists. For the liveness-to-safety result, the key guess is which state is the loop-closing state. The same idea shows up in the Lal-Reps construction for analyzing concurrent software, where the guess is the correct values of the global variables when context switches happen. The first paper gives an easy-to-read summary of three different constructions (and a bunch of experimental results -- looking back at this work, I think there's room for a good thesis here on a better performing translation). The second paper is the actual Lal-Reps paper.

Week 10:

For predicate abstraction, I'm going to assign:
Satyaki Das, and David L. Dill, "Successive Approximation of Abstract Transition Relations," Proc. of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS), June 2001.
This paper is a compromise assigned reading between the original paper on predicate abstraction (see below) and more recent papers with fancier heuristics. Section 2 is a good review of the idea of (conservative) abstraction in general, and this paper still gets cited quite a bit.

The original paper on predicate abstract:
Susanne Graf, and Hassen Saidi, "Construction of Abstract State Graphs with PVS", Conference on Computer-Aided Verification (CAV), 1997, Springer LNCS 1254. (Optional)
is also a great paper, and if you're interested in the idea, you should take a look as well.

Thomas Ball, Sriram K. Rajamani, "Bebop: A Symbolic Model Checker for Boolean Programs", SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, August/September 2000, pp. 113-130. This paper describes computing reachability over "Boolean programs", which are essentially pushdown automata. This was the original model-checking engine behind Microsoft's SLAM project, which has evolved into production use in Microsoft's Static Driver Verifier.

Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani, "Automatic Predicate Abstraction of C Programs", PLDI 2001, SIGPLAN Notices 36(5), pp. 203-213. This paper describes mapping real C programs to Boolean programs, using predicate abstraction. (Optional) (This paper basically "concretizes" (pun, haha) the connection between the more theoretical work on predicate abstraction and Boolean programs with actual software.)

Week 11:

Hmm... was this term short by a week? I did start counting at 0, but still, I think there are usually more weeks. Anyway, we finished the Bebop paper on Monday, and for Wednesday, folks asked for some coverage of parameterized verification.

I find this a very hard topic to cover, as there's quite a large literature, but it's very fragmented, with different communities that don't interact that much, using different formalism and techniques. There's also a big dichotomy between a fairly well-developed literature, with some really cool theoretical results, but not scalable to practical systems, versus a literature of techniques applied to more practical-sized systems, but relying on some ad hoc manual effort.

For your reference, I'll suggest two optional readings:

• My impression is that you all are more interested in the techniques with practical application, so I'll focus on this paper, which describes a technique that I know is used on real, industrial cache coherence protocols. Ching-Tsun Chou, Phanindra K. Mannava, Seungjoon Park, "A Simple Method for Parameterized Verification of Cache Coherence Protocols", Formal Methods in Computer-Aided Design (FMCAD), 2004, pp. 382-398. (BTW, I found a non-paywalled, unofficial link to the PDF online here, but you should be able to access the official link for free via UBC libraries.)
• And for broader survey of other techniques (and a great starting point for a literature search), look for Chapter 21 in the Handbook of Model Checking: Parosh Aziz Abdulla, A. Prasad Sistla, Muralidhar Talupur, "Model Checking Parameterized Systems", Chapter 21 in the Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem, Eds., Springer, 2018. I know this is available via UBC libraries (do a search for the title and authors), as I'm working from home and had to grab an electronic copy.

Week 9 (Guest Lectures by Mark Greenstreet, Itrat Akhter, and Carl Kwan):

Week 12: TBD

Vaastav asked for some coverage of formal verification of probabilistic systems. This paper is a good introduction:
L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala, "Symbolic Model Checking of Concurrent Probabilistic Processes Using MTBDDs and the Kronecker Representation", 6th International Worskshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000) LNCS Vol. 1785.
This is also a good chance to introduce influential work that came directly out of a CPSC 513 project. Robert St. Aubin and Jesse Hoey were in 513, and this work started as their course project and became the fastest stochastic planner available. Stochastic planning is a closely related problem to verification of probabilistic systems.
Jesse Hoey, Robert St. Aubin, Alan Hu, Craig Boutilier, "SPUDD: Stochastic Planning Using Decision Diagrams", 15th Conference on Uncertainty in Artificial Intelligence (UAI'99), pp. 279-288.

Week 13: Project Presentations!

We'll have signups for your project presentations on November 27 and November 29. We'll schedule people on 15-minute intervals, so aim for about 10-12 minutes per project (individual or group).

Week 8

Sam Bayless, Celina G. Val, Thomas Ball, Holger H. Hoos, Alan J. Hu, "Efficient Modular SAT Solving for IC3", Formal Methods in Computer-Aided Design (FMCAD), 2013, pp. 149-156. This is an amazing paper, by some truly brilliant researchers, which brings together ideas from SAT, SMT, BMC, IC3, interpolation, induction, and probably a few other ideas from the class that I can't think of right now... (Optional) (All joking aside, I really love how this paper ties together a whole bunch of other ideas. However, I can't justify it as a must-read in our limited time.)

Week 10:

OK, this is a short week (only 1 lecture) due to Remembrance Day. I know that people voted not spend time on hybrid systems, but I think you should get some exposure to the basics. I'm going to skip most of the details (usually, I'd spend about 2 weeks on this), and then try to condense about 3 lectures worth of material into one day. :-) We'll basically just look at basic concepts and definitions. For your reference, these are a great set of lecture notes to introduce continuous and hybrid systems, developed by John Lygeros of the University of Patras: John Lygeros, "Lecture Notes on Hybrid Systems", Notes for an ENSIETA short course, February 2-6, 2004. . (Optional) (This document appears to be floating around unpublished. Obviously, we don't have time to go through all of this, but these notes are provided as a background reference for you.

In the unlikely event that we have some spare time, Alur-Dill timed automata are a very cool special case of hybrid systems: Rajeev Alur, Costas Courcoubetis, and David Dill, "Model-Checking in Dense Real-Time", Information and Computation, May 1993, pp. 2-34. (Optional)

Possibly Later: