1. Books
    1. Verification of sequential and concurrent programs. Apt, Olderog
    2. Verification of Reactive Systems. Klaus Schneider
  2. Relv.Relt.Topics
    1. BIP - Sifakis
    2. Henzinger
    3. AVACS
    4. SAT/SMT solvers
    5. A.Burns - Timeband
    6. Static analysis
    7. Decision procedures
    8. Design patterns?
    9. OpenLicenseSociety-OpenVE
  3. Papers
    1. Lundqvist
    2. Bruneton, INRIA
    3. Axiomatic Treatment of Partial Correctness, Brookes
    4. "Lamport on Owicki-Gries"
    5. Douglas Howe
    6. Burns, Lin
  4. Runtime model checking
    1. Utah: 'inspect' tool
    2. Godefroid: DPOR
  5. Concurrency
    1. C
      1. VCC
        1. VCC+Assembly code
      2. Chalice
      3. C+Isabelle (non-conc)
    2. Ada
      1. Inria,Bruneton
  6. Temporal Logics
    1. mu-calculus
      1. LTL
      2. CTL
    2. Interval temporal logic
      1. duration calculus
  7. Design by contract
    1. VCC
    2. SPARK
  8. ADA
    1. ASIS: Ada Semantic Interface Specification
    2. Run-time system
      1. Lunqvist work
  9. Real-Time
    1. Formal Specification + Scheduling : 'Metzner'
      1. From high-level spec (CSP-OZ-DC)
‎PhD research‎Runtime model checking‎Utah: 'inspect' tool‎Godefroid: DPOR‎Concurrency‎C‎VCC‎VCC+Assembly code‎Chalice‎C+Isabelle (non-conc)‎Ada‎Inria,Bruneton‎Temporal Logics‎mu-calculus‎LTL‎CTL‎Interval temporal logic‎duration calculus‎Design by contract‎VCC‎SPARK‎ADA‎ASIS: Ada Semantic Interface ‎Specification‎Run-time system‎Lunqvist work‎Real-Time‎Formal Specification + Scheduling : '‎Metzner'‎From high-level spec (CSP-OZ-DC)‎Books‎Verification of sequential and concurrent ‎programs. Apt, Olderog‎Verification of Reactive Systems. Klaus ‎Schneider‎Relv.Relt.Topics‎BIP - Sifakis‎Henzinger‎AVACS‎SAT/SMT solvers‎A.Burns - Timeband‎Static analysis‎Decision procedures‎Design patterns?‎OpenLicenseSociety-OpenVE‎Papers‎Lundqvist‎Bruneton, INRIA‎Axiomatic Treatment of Partial ‎Correctness, Brookes‎"Lamport on Owicki-Gries"‎Douglas Howe‎Burns, Lin‎unifying?‎?‎? Owicki-Gries style?‎? history variables --- control state ?
Note
PhD research
Sheet 1