User Tools

Site Tools


readinggroup:spring08

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

readinggroup:spring08 [2014/03/03 19:30] (current)
cschuster Moved from readinggroup
Line 1: Line 1:
 +====Spring 2008====
  
 +  * **Apr 2**
 +    * Discussion of possible topics
 +      * concurrency & geometry
 +      * popl 08 papers
 +      * model checking
 +      * et cetera
 +
 +  * **Apr 8: Geometry and Concurrency**
 +    * [[http://​citeseer.ist.psu.edu/​goubault00geometry.html | Geometry and Concurrency:​ A User's Guide]]. Eric Goubault. Mathematical Structures in Computer Science (2000).
 +    * [[http://​opera.cs.uiuc.edu/​paper/​asplos122-lu.pdf | Learning from Mistakes - A Comprehensive Study on Real World Concurrency Bug Characteristics]]. Lu, Park, Seo, Zhou. ASPLOS 2008.
 +
 +  * **Apr 15: Model Checking: Past and Present**
 +    * [[http://​www.springerlink.com/​content/​w1778u28166t2677/​ | Design and synthesis of synchronization skeletons using branching time temporal logic]]. Clarke and Emerson. LNCS Logic of Programs, 1982.
 +    * [[http://​www.havelund.com/​Publications/​ase00.pdf | Model Checking Programs]]. Visser, Havelund, Brat, Park, Lerda. International Journal on Automated Software Engineering 2003.
 +
 +  * **Apr 22: Concurrency and Version Control**
 +    * [[http://​darcs.net/​manual/​node8.html | The Theory of Patches]]. David Roundy. Darcs Manual 2.0.0 (+ 29 patches), retrieved 2008.
 +    * [[http://​www.cs.nott.ac.uk/​~wss/​Publications/​PrincipledVersionControl.pdf | A Principled Approach to Version Control]]. Loh, Swierstra, Leijen. Draft, 2007.
 +    * [[http://​featherstitch.cs.ucla.edu/​publications/​featherstitch-sosp07.pdf | Generalized File System Dependencies]]. C Frost, M Mammarella, E. Kohler, A de los Reyes, S Hovsepian, A Matsuoka, L Zhang. SOSP 2007.
 +
 +  * **Apr 29: Abstract Interpretation**
 +    *[[http://​portal.acm.org/​citation.cfm?​id=512973&​dl= | Abstract Interpretation:​ A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation Of Fixpoints]]. P Cousot, R Cousot. POPL 1977. 
 +    * Optional. [[http://​portal.acm.org/​citation.cfm?​id=234528.234740 | Abstract Interpretation]]. P Cousot. ACM Computing Surveys, 1996.
 +    * Optional. [[http://​www.di.ens.fr/​~cousot/​publications.www/​CousotCousot-ASE-v6-n1-p69--95-1999.pdf | Refining Model Checking by Abstract Interpretation]]. P Cousot, R Cousot. Automated Software Engineering,​ 6, 69–95 (1999). ​
 +    * Reference. [[http://​www.cs.berkeley.edu/​~necula/​cs263/​lectures/​lecture10-ai.pdf | Abstract Interpretation slides]]. G Necula. [[http://​www.cs.berkeley.edu/​~necula/​cs263/​lectures.shtml | CS263 (2007)]].
 +    * Reference. [[http://​www.cs.berkeley.edu/​~necula/​cs263/​lectures/​lecture04-densem.pdf | Denotational Semantics slides]]. G Necula. [[http://​www.cs.berkeley.edu/​~necula/​cs263/​lectures.shtml | CS263 (2007)]].
 +
 +  * **May 6: Abstraction and Refinement for Model Checking**
 +    * [[http://​portal.acm.org/​citation.cfm?​id=186025.186051 | Model Checking and Abstraction]]. E Clarke, O Grumberg, D Long. TOPLAS 1994.
 +    * [[http://​www.springerlink.com/​index/​d833527r467g7261.pdf | Counterexample-Guided Abstraction Refinement]]. E Clarke, O Grumberg, S Jha, Y Lu, H Veith. CAV 2000. 
 +    * Optional. [[http://​www.kenmcmil.com/​pubs/​TACAS03.pdf | Automatic Abstraction without Counterexamples]]. K McMillan, N Amla. TACAS 2003.
 +    * Reference. [[http://​www.iro.umontreal.ca/​~cerny/​IFT6222/​6-Omega.2pp.991103.pdf | Lecture notes]] on omega-automata,​ buchi/​muller automata, L-processes. [[http://​www.iro.umontreal.ca/​~cerny/​index-presentations_990907.html | Eduard Cerny]]. 1999. 
 +
 +  * **May 13: Random Testing Techniques**
 +    * [[http://​cm.bell-labs.com/​who/​god/​public_psfiles/​pldi2005.pdf | DART: Directed Automated Random Testing]]. P Godefroid, N Klarlund, K Sen. PLDI 2005. 
 +    * [[http://​portal.acm.org/​citation.cfm?​id=1190226 | Compositional Dynamic Test Generation]]. P Godefroid. POPL 2007.
 +
 +  * **May 20: Formalization / Java Model Checking**
 +    * Coq/​Velodrome writeup for workshop
 +    * [[http://​citeseer.ist.psu.edu/​725283.html | Formalization and Verification of a Mail Server in Coq]]. R Affeldt, N Kobayashi. International Symposium on Software Security, 2002.
 +    * [[http://​citeseer.ist.psu.edu/​affeldt04coq.html | A Coq Library for Verification of Concurrent Programs]]. ​ [[http://​staff.aist.go.jp/​reynald.affeldt/​bib.html | R Affeldt]], [[http://​www.kb.ecei.tohoku.ac.jp/​~koba/​publications.html | N Kobayashi]]. 4th International Workshop on Logical Frameworks and Meta-Languages (LFM 2004).
 +    * [[http://​citeseer.ist.psu.edu/​290608.html | Model-Checking Multi-Threaded Distributed Java Programs]]. [[http://​www.cs.sunysb.edu/​~stoller/​publications.html | S Stoller]]. International Journal on Software Tools for Technology Transfer, 2000.
 +  * **May 27: Partial-Order Reduction**
 +    * [[http://​www.springerlink.com/​index/​H2K6245784Q12190.pdf | Formal Verification of a Partial-Order Reduction Technique for Model Checking]]. C Chou, D Peled. Journal of Automated Reasoning, 1999.
 +    * [[http://​www.springerlink.com/​index/​a379042kg8847840.pdf | Distributed Dynamic Partial Order Reduction based Verification of Threaded Software]]. Y Yang, X Chen, G Gopalakrishnan,​ RM Kirby. Workshop on Model Checking Software (SPIN 2007).
 +    * (Optional) [[http://​www.springerlink.com/​index/​KH6B21UDVGUTJJVH.pdf | State Space Reduction Using Partial Order Techniques]]. ​ EM Clarke, O Grumberg, M Minea, D Peled. International Journal on Software Tools for Technology Transfer, 1999.
 +  * **June 5 (Thursday): PLDI papers: A Potpourri on Concurrency,​ Model Checking, Transactional Memory** ​
 +    * [[http://​www.research.ibm.com/​people/​e/​eyahav/​papers/​pldi08.pdf | Deriving Linearizable Fine-Grained Concurrent Objects]]. Martin Vechev, Eran Yahav. PLDI 2008.
 +    * [[http://​infoscience.epfl.ch/​record/​117513 | Model Checking Transactional Memories]]. R Guerraoui, ​ T Henzinger, V Singh. PLDI 2008.
 +    * [[http://​portal.ku.edu.tr/​~stasiran/​publications/​pldi07.pdf | A Race and Transaction-Aware Runtime for Java]] Tayfun Elmas, Serdar Tasiran, Shaz Qadeer. PLDI 2007.
 +
 +  * Queue of papers
 +    * 0-1 Principle / Parallel Prefix Computation (POPL 08)
 +    * dirt to shovels (popl 08) & its predecessor,​ PADS
 +    * iComment, movi
 +    * SMT: Back to the Future (popl 08)
 +    * Galois connections and Computer Science Applications
 +    * Pnueli'​s translation validation paper ('98)
 +    * Formal Verification of Translation Validators
 +    * Dynamo ​
 +    * Denali superoptimizer
readinggroup/spring08.txt · Last modified: 2014/03/03 19:30 by cschuster