| Date | Speaker | Topic |
|---|---|---|
| Jan 16, 2009 Newell-Simon 1507 2:00 pm |
Arie Gurfinkel
Sagar Chaki |
Combining Predicate and Numeric Abstraction for Software Model Checking |
| Date | Speaker | Topic |
|---|---|---|
| August 7, 2008 Wean 7220 10:00 am |
Aarti Gupta | Software Verification without Predicate Abstraction and Refinement |
| July 18, 2008 Wean 4625 CANCELLED |
Axel Legay | Computing Convex Hull by Automata Iteration |
| June 30, 2008 Wean 7220 |
Yu-Fang Chen | Automated Compositional Verification: Problems, Solutions, and Experiments |
| June 27, 2008 Newell-Simon 1507 |
Joe Hendrix | What Did I Forget? Using Equational Tree Automata to Identify Incomplete Specifications |
| Date | Speaker | Topic |
|---|---|---|
| May 2, 2008 Newell-Simon 1109 |
Jiri Simsa | On the Way to Parallel and Distributed Explicit State LTL Model Checking |
| April 25, 2008 Newell-Simon 1507 |
Sumit Kumar Jha | Iterative Relaxation Abstraction (Verification of Linear Hybrid Automata) |
| April 2, 2008 Newell-Simon 1507 |
Haakan Younes | Statistical Probabilistic Model Checking |
| February 29, 2008 Wean 7220 |
Silke Wagner | Region Stability Proofs for Hybrid Systems |
| February 22, 2008 Newell-Simon 1507 |
Byron Cook | Proving Conditional Termination |
| February 15, 2008 Wean 7220 |
Kwangkeun Yi | Sparrow System, an Industrial-Strength Bug-Finder for C |
| February 8, 2008 Wean 7220 |
Roberto Bruttomesso | Verification: From SAT to SMT(BV) |
| February 1, 2008 Wean 7220 |
Natasha Sharygina | Automated Verification of Security Policies in Mobile Code |
| Date | Speaker | Topic | December 6, 2006 | Sandeep Bhatt | Managing End-to_End Enterprise Access Policies |
|---|---|---|
| November 20, 2006 | W. Rance Cleaveland | Model-Based Validation of Embedded Software |
| November 1, 2006 | Sriram K. Rajamani | Rigorous Software Engineering |
| October 20, 2006 | Kevin D. Jones | High-speed PHY Design and Verification in the "Real World" |
| Date | Speaker | Topic |
|---|---|---|
| February 20, 2006 | Wolfgang Windsteiger | Theorema: A Mathematical Assistant System based on Mathematica |
| February 27, 2006 | Karem Sakallah | Microprocessor Verification Based on Datapath Abstraction and Refinement |
| April 12, 2006 | Josh Berdine | Automatic Termination Proofs for Programs with Shape-Shifting Heaps |
| April 24, 2006 | Byron Cook | Automatically Proving the Termination of Software |
| May 1, 2006 | A. Prasad Sistla | Monitoring off-the-shelf Components |
| June 26, 2006 | Mahesh Viswanathan | Learning to Verify |
| Date | Speaker | Topic |
|---|---|---|
| April 30, 2001 | Ed Clarke | Verifying TTP/C |
| May 7, 2001 | Jeannette Wing | Survivability Analysis of Networked Systems |
| May 21, 2001 | Planning for ARO Kickoff Meeting | |
| June 4, 2001 | Summary of ARO Kickoff and Discussion of Case Studies | |
| June 11, 2001 | Discussion of potential NASA case study | |
| June 18, 2001 | Tools and Technology matrix for Hislop | |
| June 25, 2001 | Discussion of potential Honeywell case studies | |
| July 2, 2001 | Bruce Krogh | Matlab -- Some of our tools are based on the MATLAB Simulink tools from Mathworks. |
| July 16, 2001 | Status Report | |
| July 23, 2001 | Planning for NASA Proposal | |
| July 30, 2001 | Oded Maler | d/dt: A Tool for Reachability Analysis of Continuous and Hybrid Systems Control from Computer Science |
| August 6, 2001 | Dan Siewiorek Asim Smailagic |
Rapid Prototyping Projects |
| August 20, 2001 | Planning for NASA proposal. Status on ARO and NSF grants. | |
| August 27, 2001 | Planning for NASA proposal | |
| September 4, 2001 | Planning for NASA proposal | |
| September 11, 2001 | Planning for NASA proposal | |
| September 18, 2001 | ARO Visit and NASA proposal | |
| October 2, 2001 | Sagar Chaki | c2bp (C to binary program) tool developed at Microsoft Research Labs for software model checking. |
| October 16, 2001 | Bruce Krogh | A survey of methods for approximating hybrid system dynamics for verification |
| October 23, 2001 | Håkan Younes | Probabilistic Verification |
| October 30, 2001 | Olaf Stursberg | Modular Analysis of Discrete Controllers for Distributed Hybrid Systems |
| November 6, 2001 | Rune Jensen | Automatic Controller Synthesis via BDD-based Universal Planning |
| November 13, 2001 | Sanjit Seshia | Modular Verification of Multithreaded Software |
| November 27, 2001 |
Discussion session about high-level programming language interface to state-machine based model checkers like SMV. Relevant to this discussion:
|
|
| December 4, 2001 | Honeywell Debriefing | |
| December 11, 2001 | Rajeev Alur | Reachability Analysis of Hybrid Systems via Predicate Abstraction |
| January 22, 2002 | Bernhard Steffen | The Electronic Tool Integration Plattform Abstract / CV | Slides (PDF) www.eti-service.org |
| January 29, 2002 | Ofer Strichman | A Propositional World Abstract / CV | Slides (PowerPoint) |
| February 5, 2002 | Sagar Chaki | Software Verification via Refinement Checking Abstract | Slides (PowerPoint) |
| February 12, 2002 | Kenneth Butts | Usage Scenarios for an Automated Model Compiler Abstract |
| February 19, 2002 | Anubhav Gupta | SAT based Abstraction-Refinement using ILP and Machine Learning Techniques Abstract | Slides (PDF) |
| February 26, 2002 | Håkan Younes | Probabilistic Verification of Descrete Event Systems using Acceptance Sampling Abstract | Slides (PowerPoint) |
| March 5, 2002 | Flavio Lerda | Java PathFinder and Model Checking of Programs Abstract / CV | Slides (PowerPoint) |
| March 12, 2002 | Collin Spencer | SM2SMV: Model Checking for Stateflow Diagrams with Floating Point Variables and Complex Expressions Abstract / CV |
| March 19, 2002 | Alex David Groce | Structural Heuristics for Directed Model Checking of Java Programs Abstract |
| March 26, 2002 | Bridget Spitznagel | A partial semantics of connector augmentations: first steps Abstract | Slides (PowerPoint) |
| April 2, 2002 | Constance L. Heitmeyer | Towards Kinder, Gentler Formal Methods: Automatic Construction and Application of State Invariants Abstract / CV |
| April 2, 2002 | Myla Archer | TAME: A Kinder, Gentler Version of PVS for Proving Properties of Automata Abstract / CV |
| April 9, 2002 | Frank Pfenning | Linear Logic for the Specification of Concurrent Systems Abstract |
| April 16, 2002 | Pankaj Chauhan | Image Computation in Symbolic Verification Abstract | Slides (PowerPoint) |
| April 23, 2002 | Grant reviews / grant proposals | |
| April 30, 2002 | PI Meeting | |
| May 14, 2002 | Corina Pasareanu | Combination of Symbolic Execution and Model Checking Abstract / CV | Slides (PowerPoint) |
| May 28, 2002 | Paul Hubbard | Automatic Test Vector Generation for Hybrid Models Abstract |
| June 4, 2002 | PI Meeting | |
| June 18, 2002 | Ansgar Fehnker | Efficient Mimimal-Cost Reachability for Linearly Priced Timed Automata Abstract | Slides (PowerPoint) |
| July 2, 2002 | Sanjit Seshia | The UCLID Verification System Abstract |
| July 16, 2002 | Oded Maler | On Control with Bounded Computational Resources Abstract |
| July 23, 2002 | Orna Grumberg | Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking Abstract |
| August 13, 2002 | Joël Ouaknine | Some decidability and undecidability results for timed automata Abstract/CV | Slides |
| September 4, 2002 | Thomas Ball | Secrets of Software Model Checking Abstract |
| September 17, 2002 | Alex David Groce | What Went Wrong Abstract | Slides (PowerPoint) |
| September 24, 2002 | Karen Yorav | Modular model checking for sequential programs Abstract |
| October 1, 2002 | Joël Ouaknine | Digitisation Techniques for Timed Systems Abstract | Slides (PDF) |
| October 8, 2002 | Gianfranco Ciardo | Exploiting Structural Information for Efficient Symbolic State-Space Generation Abstract |
| October 29, 2002 | Ofer Strichman | Solving Disjunctive Linear Arithmetic with SAT Abstract |
| November 5, 2002 | Li Tan | Evidence-Based Verification Abstract |
| November 26, 2002 | Paulo Tabuada | Automatic synthesis for embedded systems Abstract |
| December 3, 2002 | Natalia Sharygina | Model Checking Large-Scale Software Systems Abstract | Slides (PowerPoint) |
| December 10, 2002 | Ansgar Fehnker | Introduction to Simulink/Stateflow Abstract |
| January 14, 2003 | Dirk Beyer | Efficient BDD Representation for Reachability Analysis of Timed Automata Abstract | Slides (PDF) |
| January 21, 2003 | Oliver Niese | Automated Functional Testing of Web-based Applications Abstract |
| Markus Wuebben | The Electronic Tool Integration - Next Generation Abstract |
|
| February 4, 2003 | Joël Ouaknine | Revisiting Digitization, Robustness, and Decidability for Timed Automata Abstract | Slides (PDF) |
| February 11, 2003 | Marsha Chechik | CANCELED Multi-Valued Model-Checking: Theory, Implementation and Applications Abstract |
| February 25, 2003 | K. Subramani | An Analysis of Quantified Linear Programs Abstract |
| March 18, 2003 | Edjard de Souza Mota | Verification Agent: An Experiment Joining Formal Verification and CASE Tools Abstract |
| April 15, 2003 | Sanjit Seshia | Translating Quantified Separation Logic to Quantified Boolean Logic Abstract |
| Apr 22, 2003 | Dong Wang | SAT based Abstraction Refinement for Hardware Verification Abstract |
| May 20, 2003 | Alex David Groce | Explaining Counterexamples: Causal Analysis and Comparison of Transition Sequences Abstract |
| May 27, 2003 | Sanjit Seshia | A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions Abstract |
| August 5, 2003 | Corina Pasareanu Dimitra Giannakopoulou |
Automated assume-guarantee reasoning for component verification Abstract / CV |
| August 12, 2003 | Amir Pnueli | A Compositional Approach to Verification (both Deductive and Algorithmic) of CTL* Properties Abstract | Slides: PostScript, PDF |
| August 19, 2003 | Oded Maler | On Timing Analysis of Combinational Circuits Abstract | Slides (PostScript) |
| August 26, 2003 | Goran Frehse | Verification of Linear Hybrid Automata using Simulation Relations Abstract/CV |
| September 2, 2003 | Joël Ouaknine | On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap Abstract/CV | Slides (PDF) |
| September 9, 2003 | George Pappas | Temporal logic control of continuous systems Abstract | Slides (PDF) |
| September 16, 2003 | Klaus Schmidt | High-Level Abstraction of Concurrent Finite Automata for the Purpose of Hierarchical Control Abstract / CV | Slides (PowerPoint) |
| September 30, 2003 | Ashish Tiwari | Symbolic techniques for analysis of hybrid systems Abstract / CV |
| October 29, 2003 | Pete Manolios | Refinement in Branching Time & Applications to Pipelined Machine Verification Abstract/CV |
| January 13, 2004 | Daniel Kroening | Verification of low-level ANSI-C Programs |
| March 9, 2004 | Håkan Younes | Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study Paper | Abstract/Bio |
| March 23, 2004 | Jin Yang | Compositional Specification and Model Checking in GSTE Abstract/Bio | Slides (PowerPoint) |
| March 29, 2004 | Alkis Konstantellos | Special meeting: European Embedded Systems Projects and Opportunities for EU-US Collaboration |
| March 30, 2004 | Goran Frehse | Assume/Guarantee Reasoning for Hybrid I/O Automata Abstract/CV |
| April 6, 2004 | Massimo Tivoli | A coordinators synthesis approach for reliability enhancement in component-based systems Abstract/CV |
| April 13, 2004 | José Meseguer | Rewriting Logic Based Semantics and Analysis of Concurrent Programs Abstract/CV |
| May 4, 2004 | Ferucio Laurentiu Tiplea | Abstractions of Data Types Abstract/CV | Slides (PDF) |
| May 20, 2004 | Carl Seger | Integrating Design and Validation Abstract/CV |
| July 6, 2004 | Sanjit Seshia | Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds Abstract |
| February 28, 2005 | Ofer Strichman | A Decision Procedure for Equality Logic Slides: PowerPoint |
| March 2, 2005 | Shenbing Jiang | Failure Diagnosis of Discrete Event Systems: A Temporal Logic Approach Slides: PDF | Paper: PDF |
| March 4, 2005 | Willem Visser | Towards Combining Explicit-state Model Checking, Symbolic Execution, and Predicate Abstraction Slides: PowerPoint |
| March 14, 2005 | William L. Scherlis | Direct Software Assurance Resource: The Fluid Project |
| March 21, 2005 | Jonathan Aldrich | Dependable Real-Time and Embedded Space Software |
| March 28, 2005 | Stefan Schwoon | Interprocedural Dataflow Analysis with Weighted Pushdown Systems |
| April 21, 2005 | Thanyapat Sakunkonchak | Formal Verification Techniques Targeting C Based VLSI Design Descriptions |
| April 29, 2005 | Kedar Namjoshi | From Model Checking to Proof Checking ... and Back |
| September 26, 2005 | Alan Hu | Empirically Efficient Verification for a Class of Infinite State Systems |
| October 3, 2005 | Randal E. Bryant | Decision Procedures Customized for Formal Verification |
| October 31, 2005 | Lenore Zuck | Microcode Verification |
| November 7, 2005 | Paulo Tabuada | On the Synthesis of Correct-by-Design Embedded Control Software |
| November 14, 2005 | Manuvir Das | Software Excellence via Program Verification at Microsoft Slides: PowerPoint |
| December 2, 2005 | Andreas Tiemeyer | Generalized Symbolic Trajectory Evaluation |
| December 12, 2005 | Flavio Lerda | Validation of Control Software |
| Maintainer | [ Home ] |
| Last modified: Tues Dec 16 11:22:23 EDT 2008 |