We aim to gain fundamental new insights into the emergent behavior of complex biological and embedded systems through the use of revolutionary, highly scalable and fully automated modeling and analysis techniques.

Gerard Holzmann's paper featured in Feb. issue of Communications of the ACM January 29, 2014. This article discusses some of the precautions the JPL flight software team took to improve the reliability of the Curiosity rover on Mars.

Bud Mishra featured on cover of Royal Society Interface November 25, 2013.

Dr. Natasa Miskov-Zivanov and Dr. James Faeder are featured in the current issue of Science Signaling for their research on – "The Duration of T Cell Stimulation Is a Critical Determinant of Cell Fate and Plasticity." November 20, 2013. (Podcast is available here)

Formal Verification of Behavioral Models of Phase-Locked Loops (PLLs) Made Tractable With New Methods for Computing Reachable Sets for Hybrid Dynamic Systems. November 4, 2013

CMACS Research Featured on Cover of Transactions on Computational Biology and Bionformatics. September 26, 2013

CMACS Researchers Developed a New Framework for Verifying Hybrid Systems. October 15, 2012

CMACS Researchers Directly Involved in the Development of the Complex Software for the Curiosity Rover. August 30, 2012

CMACS Researchers Co-Author Nature Paper on Low-Energy Control of Electrical Turbulence in the Heart. July 25, 2011

CMACS Researchers Perform First Automated Formal Analysis of Realistic Cardiac Cell Model. January 26, 2011

Hot off the press:
Logical Analysis of Hybrid Systems by CMACS researcher André Platzer

Metalibm: a code generator for parametrized mathematical functions PDF
Olga Kupriianova, Paris-6 University
11/7/2014, 11:30am, GHC 8115

What can be formally addressed for industrial control systems? PDF
Xiaoqing Jin, Toyota
9/17/2014, 10:00am, GHC 9115

Advanced Analysis for Industrial Embedded Control Designs PDF
Jim Kapinski, Toyota
4/29/2014, 10:00am, GHC 6501

On the complexity of minimizing probabilistic and quantum automata PDF
Paulo Mateus, Departamento de Matemática, Instituto Superior Técnico
2/28/2014, 1:30pm, GHC 8102

Tricks with PRISM: Probabilistic Model Checking on Structured Models PDF
David Musliner, SIFT
12/18/2013, 10:00am, GHC 9115

Diversely Enumerating Solutions to Synthesis Problems PDF
Ethan Jackson, Microsoft Research
11/15/2013, 11:00am, GHC 7501

Towards formal validation of aerospace systems PDF
Eric Feron, School of Aerospace Engineering, Georgia Inst. of Technology
9/13/2013, 1:30pm, GHC 6501

Specification Mining for Controller Verification and Synthesis PDF
Sanjit Seshia, Dept. of EECS, Univ. of California, Berkeley
5/22/2013, 4:00pm, GHC 8102

UFO: From Under-approximations to Over-approximations and Back PDF
Arie Gurfinkel, Carnegie Mellon University, Software Engineering Institute
5/13/2013, 2:00pm, GHC 6115

More Seminars

Ed Clarke receives Franklin Institute's Bower Award for 2014 April 24, 2013

One week intensive courses on Foundations of Cyber-Physical Systems at i-MAP, Portugal in March 2014 and ENS Lyon in January 2014

New undergraduate course, Foundations of Cyber-Physical Systems, Fall 2013

2014 NSF-CMACS Undergraduate Workshop on Cellular Signaling Pathways. Writeup and Photos from January 24, 2014

Patrick and Radhia Cousot receive the ACM SIGPLAN Achievement Award November 25, 2013

CMACS/AVACS Workshop & PI Meeting will take place at Carnegie Mellon University, November 20-22, 2013

The Technology that Could Save Robotic Surgery Millions: Software diagnostic research debugs robotic surgical systems by Henry Lenard for Robotic Business Review, May 3, 2013

CMACS PI Gerard Holzmann Awarded 2012 NASA Exceptional Engineering Achievement Medal.

CMACS Fall 2012 PI Meeting will take place at Stony Brook University, October 18-19, 2012

More News