Monday, December 12, 2011
Antoine Miné, Junior researcher, École Normale Supérieure, Paris, FranceAstréeA: A static analyzer for embedded multi-threaded C programs
Abstract: In this talk, we present an efficient static analysis based on Abstract Interpretation that aims at proving the absence ...
Thursday, November 24, 2011
Misha Aizatulin, PhD Student, Open University, United KingdomExtracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution
Abstract: Consider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic so...
Wednesday, November 2, 2011
Ivan Beschastnikh, PhD candidate, University of Washington, USALeveraging Existing Instrumentation to Automatically Infer Invariant-Constrained Models
Abstract: Computer systems are often difficult to debug and understand. A common way of gaining insight into system behavior is to...
Thursday, October 20, 2011
Matthieu Sozeau, PhD Student, INRIA Rocquencourt, FranceFirst-Class Type Classes for programs and proofs
Abstract: Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and fo...
Friday, October 7, 2011
Dejan Kostic, Assistant Professor, Ecole Polytechnique Federale de Lausanne, SwitzerlandOnline Testing of Deployed Federated and Heterogeneous Distributed Systems
Abstract: It is notoriously difficult to make distributed systems reliable. This becomes even harder in the case of the widely-dep...
Monday, September 12, 2011
Martin Wirsing (in cooperation with Matthias Hoelzl), Professor, Ludwig-Maximilians University of München, GermanyAdaptation and Awareness in Ensembles
Abstract: The ASCENS project (http://www.ascens-ist.eu/) researches foundations of and software-engineering methods for ensembles ...
Monday, September 12, 2011
Rodrigo Rodrigues, Assistant Research Professor, Max Planck Institute for Software Systems, GermanyGaining Customer Trust in Cloud Services with Excalibur
Abstract: Despite the benefits of cloud computing, its potential customers are concerned with data mismanagement risks that stem f...
Friday, June 24, 2011
Nazareno Aguirre, Professor, Universidad Nacional de Río IV, ArgentinaIncorporating Coverage Criteria in Bounded Exhaustive Black Box Test Generation of Structural Inputs
Abstract: The automated generation of test cases for heap allocated, complex, structures is particularly difficult. Various state ...
Friday, May 20, 2011
Reinhard Wilhelm, Professor, Saarland University, GermanyOngoing Work and Open Questions in Timing Analysis
Thursday, April 28, 2011
Giorgio Delzanno, Associate Professor, Università di Genova, ItaliaMonotonic Approximations in Parameterized Verification
Abstract: In the talk I will present a series of abstractions that can be used to obtain approximated verification algorithms for ...
Thursday, April 7, 2011
Natasha Sharygina, Assistant Professor, Università della Svizzera Italiana, Lugano, SwitzerlandLocal proof transformations for flexible interpolation and proof reduction
Abstract: Model checking based on Craig’s interpolants ultimately relies on efficient engines, such as SMT-Solvers, to log p...
Monday, April 4, 2011
Pavithra Prabhakar, PhD Student, University of Illinois at Urbana Champaign, USAApproximations for Verification of Cyber Physical Systems
Abstract: Cyber Physical Systems (CPS) is a term broadly used to define systems in which the cyber world consisting of computation...
Wednesday, March 16, 2011
Deepak Kapur, Professor, University of New Mexico, USAInduction, Invariants, and Abstraction
Abstract: Invariants play a key role in verifying properties of imperative programs. Inductive reasoning is essential to verifying...
Wednesday, March 16, 2011
Doron Peled, Professor, Bar Ilan University, IsraelKnowledge based synthesis of control for distributed systems
Abstract: We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints...
Tuesday, March 15, 2011
Isil Dillig, PhD Student, Stanford University, USAPrecise and Fully-Automatic Verification of Container-Manipulating Programs
Abstract: One of the key challenges in automated software verification is obtaining a conservative, yet sufficiently precise under...
Monday, March 14, 2011
Thomas Dillig, PhD Student, Stanford University, USAProgram Paths Simplified: Scalable Path-Sensitive Analysis without Heuristics
Abstract: A path-sensitive static analysis considers each possible execution path through a program separately, potentially yieldi...
Friday, March 4, 2011
Vijay Ganesh, Postdoctoral Scholar, MIT Cambridge, MA, USASolvers for Software Reliability and Security
Abstract: Constraint solvers such as Boolean SAT or modular arithmetic solvers are increasingly playing a key role in the construc...
Tuesday, March 1, 2011
Raul Santelices, PhD Student, Georgia Institute of Technology, USAChange-effects Analysis for Effective Testing and Validation of Evolving Software
Abstract: Software is constantly modified during its life cycle, posing serious risks because changes might not behave as expected...
Tuesday, February 22, 2011
Graham Steel, Researcher, INRIA Rocquencourt, FranceAttacking and Fixing PKCS#11 Security Tokens
Abstract: We show how to extract sensitive cryptographic keys from a variety of commercially available tamper resistant cryptograp...
Friday, February 11, 2011
Vasu Singh, Postdoctoral Scholar, Institute of Science and Technology (IST)Exporting the Art of Formal Verification
Abstract: Formal verification is described as the branch of computer science that formally establishes the correctness of systems....
Monday, February 7, 2011
Filip Pizlo, PhD Student, Purdue University, USAFragmentation Tolerant Real Time Garbage Collection
Abstract: Managed languages such as Java and C# are being considered for use in hard real-time systems. A hurdle to their widespre...
Tuesday, January 18, 2011
David Basin, Professor, ETH Zurich, SwitzerlandPolicy Monitoring in First-order Temporal Logic
Abstract: In security and compliance, it is often necessary to ensure that agents and systems comply to complex policies. An examp...