11/7/2014
11:30am

GHC 8115

Olga Kupriianova, Paris-6 University

Metalibm: a code generator for parametrized mathematical functions PDF

9/17/2014
10:00am

GHC 9115

Xiaoqing Jin, Toyota

What can be formally addressed for industrial control systems? PDF

4/29/2014
10:00am

GHC 6501

Jim Kapinski, Toyota

Advanced Analysis for Industrial Embedded Control Designs PDF

2/28/2014
1:30pm

GHC 8102

Paulo Mateus, Departamento de Matemática, Instituto Superior Técnico

On the complexity of minimizing probabilistic and quantum automata PDF

12/18/2013
10:00am

GHC 9115

David Musliner, SIFT

Tricks with PRISM: Probabilistic Model Checking on Structured Models PDF

11/15/2013
11:00pm

GHC 7501

Ethan Jackson, Microsoft Research

Diversely Enumerating Solutions to Synthesis Problems PDF

9/13/2013
1:30pm

GHC 6501

Eric Feron, School of Aerospace Engineering, Georgia Inst. of Technology

Towards formal validation of aerospace systems PDF

5/22/2013
4:00pm

GHC 8102

Sanjit Seshia, Dept of Electrical Engineering and Computer Sciences at University of California, Berkeley

Specification Mining for Controller Verification and Synthesis PDF

5/13/2013
2:00pm

GHC 6115

Arie Gurfinkel, Carnegie Mellon Univeristy, Software Engineering Institute

UFO: From Under-approximations to Over-approximations and Back PDF

5/10/2013
3:30am

GHC 8102

Sayan Mitra, University of Illinois at Urbana-Champaign, Dept. of Electrical and Computer Engineering

From Simulation to Verification of Hybrid and Distributed Systems PDF

4/3/2013
1pm

GHC 7501

Eric Goubault and Sylvie Putot, CEA LIST Institute / Ecole Polytechnique

Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and FLUCTUAT PDF

1/14/2013
2pm

GHC 9115

Laura R. McCabe, Dept of Physiology, Michigan State Univ.

Role for intestine-bone signaling pathways in regulating osteoporosis PDF

11/12/2012
11am

GHC 8102

Bing Liu, Computer Science Dept., Carnegie Mellon University

Probabilistic Approximation Techniques for Biopathway Modeling PDF

10/24/2012
10am

GHC 9115

Azadeh Farzan, Computer Science Dept., Univ. of Toronto

Data Flow Graphs for Verification of Concurrent Programs PDF

10/5/2012
2pm

GHC 8102

Clark Barrett, Computer Science Dept., New York University

Beyond DPLL(T): A new model-based approach to search in SMT and its application to solving nonlinear arithmetic PDF

09/28/2012
2pm

GHC 8102

Thomas Forster, Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, U.K.

Representing Continuous Games as Discrete Games PDF

09/14/2012
2pm

GHC 6501

Richard Banach – Professor, Department of Computer Science, University of Manchester

A Refinement Based Approach to Hybrid Systems: Basics and Event-B Design PDF

05/25/2012
2pm

GHC 6501

P. S. Thiagarajan (Thiagu) – Professor, Department of Computer Science, National University of Singapore

Probabilistic Approximations of ODEs Based Bio-pathways Dynamics PDF

05/14/2012
2pm

GHC 8102

Gianfranco Ciardo - Department of Computer Science and Engineering, Bourns College of Engineering, University of California at Riverside PDF

Exploiting Model Structure to Encode Transition Relations and Transition Rate Matrices

4/23/2012, 2:00pm

GHC-6121

Robin Dowell, Assistant Professor, University of Colorado - MCD Biology

Automatically generating stochastic models of transcriptional regulation (PDF)

04/13/2012, 2pm

GHC-4405

Pierre-Loic Garoche - Visiting Assistant Professor at University of Iowa On leave from ONERA-French Aerospace Laboratory

Kind-AI: When abstract interpretation and SMT-based model-checking meets (PDF)

03/19/2012, 3:30 PM

GHC-3305

Robert Constable - Cornell Univ., Computer Science Department

The Rise of Type Theory:  From Principia Mathematica to Constructive Type Theory, circa 1910-2010 (PDF)

2/27/2012, 2:00PM

GHC-6501

Masahiro Fujita - University of Tokyo, VLSI Design and Education Center

Tsunami Simulation on FPGA and its Analysis Based on Statistical Model Checking  (PDF)

12/12/2011, 2:00PM

GHC-6501

Cesar A. Munoz
NASA-Langley Research Center, Hampton, VA

Formally Solving Nonlinear Arithmetic Problems With Bernstein Polynomi

12/02/2011, 2:00PM

GHC-6501

Jan-David Quesel, Research Assistant/Grad student, University of Oldenburg, Dept. of Computing Science

Crossing the bridge between similar games (PDF)

09/16/2011, 2:00PM

GHC-6501

Tongtong Wu - Assistant Professor, Department of Epidemiology and Biostatistics, School of Public Health, University of Maryland-College Park

A Transcriptome Analysis by Lasso Penalized Cox Regression for Pancreatic Cancer Survival

09/02/2011, 1:30PM

GHC-6501

Yanni Kouskoulas - Johns Hopkins University, Applied Physics Laboratory

Certifying the Concurrent State Table Implementation in a Surgical Robotic System

07/22/2011, 2pm

GHC-8102

Masahiro Fujita - University of Tokyo, VLSI Design and Education Center

An Energy-Efficient Patchable Accelerator For Post-Silicon Engineering Change and Debugging PDF files

07/20/2011, 2pm

GHC-8102

Goran Frehse - Universite Joseph Fourier, Grenoble

Computational Modeling and Analysis for Complex Systems Seminar (CMACS) PDF files

07/12/2011, 3pm

GHC-7101

Alexandre Donze - Verimag Laboratory, Voreppe, France

Quantitative Temporal Logics for Biological Systems

07/11/2011, 10am

GHC-8102

Sérgio Campos - Universidade Federal de Minas Gersia, Brazil

Sodium-Potassium Exchange Pump Model and Analysis with Probabilistic Model Checking  PDF files

07/8/2010
2pm

GHC 8102

Radu Grosu
Computer Science Department, Stony Brook University, New York

Predicting Emergent Behavior in Cardiac Tissue: A Grand Challenge PDF files

06/20/2011, 2pm

GHC-8102

Natasha Sharygina - University of Lugano, Formal Verification and Security Lab

Local proof transformations for flexible interpolation and proof reduction  PDF files

GHC-6501

Calin Belta, Boston University

Formal verification and synthesis of piecewise affine systems with applications to gene networks PDF files

Neda Saeedloei - University of Texas at Dallas

Modeling and Verification of Real-Time/Hybrid/Cyber-Physical Systems via Concurrent Co-inductive Constraint Logic Programming PDF files

Zhengwei Qi, Associate Professor, Shanghai Jiao Tong University-Shanghai, China

An Online Finite LTL Model Checker for Distributed Systems PDF files

Ping Hou, Visiting SCS-CMU Postdoctoral Fellow

Finite Domain Inference Methods for Extensions of First-order Logic

Marius Minea
Politehnica University of Timisoara, Romania

Automated Detection of Guessing and Denial of Service Attacks in Security Protocols PDF slides

01/14/2011, 3:30 PM

GHC-6501

Pedro Baltazar
Security and Quantum Information Group (SQIG) Technical University of Lisbon, Portugal

How to make a logic probabilistic? PDF slides

12/10/2010, 2:00 PM

GHC-6501

Ufuk Topcu
California Institute of Technology, Department of Computing and Mathematical Sciences

Synthesis of Embedded Control Software PDF slides

12/03/2010, 2:00 PM

GHC-6501

Christel Baier, Professor
Technische Universität Dresden, Germany

On Model Checking Techniques for Randomized Distributed Systems PDF slides

11/19/2010, 2:00 PM

GHC-6501

Mahesh Viswanathan, Associate Professor
Department of Computer Science University of Illinois, Urbana-Champaign

Approximating Hybrid Systems PDF slides

11/12/2010
2:00 PM

GHC-6501

Alessio Lomuscio
Department of Computing, Imperial College, London, UK

Verification of multi-agent systems

10/25/10,
2 PM

GHC-6501

Shoichiro Fujiwara
Fujitsu Laboratories

Automatic Data Generation for Web Application Validation PDF slides

10/22/10,
2 PM

GHC-6501

Steve Marcus, Professor
Univ. Maryland, Department of Electrical and Computer Engineering, Institute for Systems Research

A Model Reference Adaptive Search Method for Global Optimization PDF slides

10/15/10,
2:30 PM

GHC-7101

Ansgar Fehnker, Senior Researcher
National Information and Communications Technology Australia

Static Analysis with Goanna - Using model checking to analyze large code bases PDF slides

10/08/2010
2 PM

GHC-6501

Quoc-Nam Tran, Professor
Lamar University (Texas State), Beaumont, Texas

Groebner Bases Computation in Boolean Rings for Model Checking and Their Applications in BioInformatics PDF slides

9/27/2010
2 PM

GHC-6501

Marta Kwiatkowska, Director Graduate
Studies, Oxford University Computing Laboratory

Automated Compositional Verification for Probabilistic Systems PDF slides

8/19/2010
3 PM

GHC-9115

Masahiro Fujita, University of Tokyo

Microprocessor verification/debugging in abstracted level and their application to post-silicon debugging

05/21/2010
2 PM

Sanjit Seshia, University of California at Berkeley

Integrating Induction and Deduction for Verification and Synthesis

05/07/2010
2 PM

GHC-6115

Matthias Althoff, ECE

04/30/2010
2 PM

GHC-6501

Marsha Chechik, University of Toronto

Monitoring and Recovery of Web Service Applications PDF slides

04/30/2010
11 AM

GHC-8102

Alongkrit Chutinan,  Mathworks Corp.

Introduction to Conditionally Executed Subsystem Semantics in Simulink

04/09/2010
2 PM

GHC-4405

Mike Whalen,  Software Engineering Center, University. of Minnesota

Semantics of Statecharts PDF slides

04/02/2010
2 PM

GHC-6501

Hiroyuki Kuwahara, SCS, Carnegie Mellon

Efficient Analysis of Dynamical Properties in Stochastic Chemical Kinetic Models. PDF slides

04/02/2010
11am

GHC-6501

Zhi Han, MathWorks, Natick, Massachusetts

Detecting Data Store Access Conflict in Simulink by Solving Boolean Satisfiability Problems

02/19/2010 – 2 PM

GHC 6501.

Vincent Danos, The University of Edinburgh,

Energy as Syntax - an attempt at a thermodynamical framework for combinatorial molecular networks. PDF slides

02/05/2010 – 2 PM

GHC 6115

Masahiro Fujita, University of Tokyo
Sree Rajan, Fujitsu Laboratories of America, Sunnyvale, CA

Model Checking Large Complex Web Applications

01/15/2010
2 PM

GHC 6501

Adam Halasz, West Virginia University
[Non]-Deterministic dynamics in cells: From multistability to stochastic switching. PDF slides

Chris J. Myers, University of Utah
Synthetic Biology: A New Application Area for Design Automation Research. PDF slides