High Integrity Language Technology
ACM SIGAda’s Annual International Conference
Nikolaj Bjorner is a Principal Researcher at Microsoft Research working in the area of Automated Theorem Proving and Software Engineering. The current main line of work is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Previously, he designed the DFSR, Distributed File System - Replication, shipped with Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, and program synthesis and transformation systems at the Kestrel Institute. He received his Master's and Ph.D. degrees in Computer Science from Stanford University.
Jeff Boleng is a research scientist in the Advanced Mobile Systems group at the Software Engineering Institute, Carnegie Mellon University, in Pittsburgh, PA, USA. His current research focus is enabling rich computing applications and data at the tactical edge. He is also researching techniques for widespread software portability and attack surface characterization of mobile devices. His past operational Air Force Experience includes evaluating and implementing SOA solutions for command and control and knowledge management applications. He is a 1991 graduate of the US Air Force Academy and has an M.S. and Ph.D. in Mathematical and Computer Sciences from Colorado School of Mines.
He can be reached via email at JLBoleng at SEI.CMU.Edu
Sagar Chaki is a senior Member of Technical Staff at the Software Engineering Institute at Carnegie Mellon University. He received a B.Tech in Computer Science & Engineering from the Indian Institute of Technology, Kharagpur in 1999, and a Ph.D. in Computer Science from Carnegie Mellon University in 2005. These days, he works mainly on model checking software for real-time and cyber-physical systems, but he is generally interested in rigorous and automated approaches for improving software quality. He has developed several automated software verification tools, including two model checkers for C programs, MAGIC and Copper. He has co-authored over 50 peer reviewed publications. More details about Sagar and his current work can be found at
Ed has been teaching Ada and object-oriented methods since 1982, and since 1986 consulting as well. He also teaches and consults on systems engineering, software engineering and architectures, the Unified Modeling Language (UML), and the C++, and Java programming languages.
Ed consulted through the University of Southern California Center for Software & System Engineering, for the U.S. Army on architecture and engineering issues relevant to the Future Combat Systems project, and for the U.S. Department of Defense on methods, processes, and tools through USC's new research center on systems engineering. He contributed to the Lean Model-Based Software Engineering (Lean MBASE) method of the USC Center for Systems & Software Engineering (CSSE). Ed led research on estimating the cost of developing secure systems for the Aerospace Corporation and the Federal Aviation Administration (FAA), and on representing and analyzing security and safety concerns at an architecture level.
Ed consulted on the definition of the Architecture Analysis & Design Language (AADL) for real-time, safety-critical systems based on the Unified Modeling Language ("UML"), and Honeywell's MetaH; the ADL that is a standard of Society of Automotive Engineers (SAE). He created the Colbert Object-Oriented Software Development method ("OOSD"), which supports analysis and design for implementation in languages such as Ada, C++, and SmallTalk. NASA Langley Research Center used OOSD for a Software Engineering Process manual, choosing OOSD partly for its strength in real-time software development.
Ed has delivered presentations at the International Society of Parametric Analysts (2006, '08), in '08 winning the Best Paper award, Tools & Methods track; Applied Computer Security Applications Conference (2005, '06); Annual COCOMO II & Software Costing Forums (2002-2008), FAA's Information Technology - Information Systems Security Research & Development Workshop (2003-2004); Object Management Group Workshops (2003-2005); Ground Systems Architecture Workshop (Los Angeles, 2003); International Conference on Reliable Software Technologies (Spain 2004, France 2003, Belgium 2001); TOOLS (2000, 1995); Ada-Europe (England, 1997); SIGAda (2003); TRI-Ada (1996, '95, '92, '89, '88); Ada UK (London, 1995); UNICOM (England, 1993); OOPSLA (Washington, D.C., 1993); Object Expo (New York, 1993; England, '92); LOOK (Denmark, 1992); OOP (Germany, 1992); SCOOP - Europe (England, 1991).
He is a graduate of the University of Michigan (M.S. Computer & Communication Sciences, 1981; B.S. (with distinction) Chemistry and Biology, 1979).
Ethan K. Jackson is a Researcher in The Research in Software Engineering (RiSE) Group at Microsoft Research. His work focuses on next-generation formal specification languages for model-based development with an emphasis on automated synthesis. He is the core researcher and engineer of the FORMULA specification language. Ethan received his PhD in Computer Science from Vanderbilt University in 2007 and his BS in Computer Engineering from the University of Pittsburgh in 2004. He joined Microsoft Research in 2007.
FORMULA is designed to have broad applicability. It is being used within Microsoft to develop DSLs for engineering and verifying critical device drivers. It is used to give semantics to hybrid systems as part of the Adaptive Vehicle Make (AVM) project (DARPA). We are applying FORMULA to synthesize models of biological systems (
http://goto.ucsd.edu/~rjhala/OBT2013/) and reason about formal privacy policies. Below is a selection of some recent and relevant literature. He is happy to provide preprints of papers that have been accepted but not yet appeared in print.
- Ethan K. Jackson, Wolfram Schulte and Nikolaj Bjorner: Theory and Implementation of Open-World Logic Programs with Constraints, (under review/ MSR Tech Report).
- Ethan K. Jackson, Gabor Simko, and Janos Sztipanovits: Diversely Enumerating System-Level Architectures, EMSOFT 2013.
- Ankush Desai, Vivek Gupta, Ethan K. Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey: P: Safe Asynchronous Event-Driven Programming, PLDI 2013.
- Ethan K. Jackson, Tihamer Levendovszky, and Daniel Balasubramanian: Automatically Reasoning about Metamodeling, Journal of Software and Systems Modeling, 2013.
- Ethan K. Jackson, Wolfram Schulte and Nikolaj Bjorner: Detecting Specification Errors in Declarative Languages with Constraints, MODELS 2012.
- Ethan K. Jackson, Nikolaj Bjorner, and Wolfram Schulte: Canonical Regular Types, ICLP 2011.
- Ethan K. Jackson, Eunsuk Kang, Markus Dahlweid, Dirk Seifert, and Thomas Santen: Components, Platforms and Possibilities: Towards Generic Automation for MDA, EMSOFT 2010.
Francesco Logozzo is a researcher in RiSE, the software engineering group at Microsoft Research, Redmond. Francesco’s ultimate goal is to make verification usable, and he strongly believes abstract interpretation is the way to achieve it. He is one of the authors of CodeContracts, the .NET contract system (API, documentation generation, runtime, and static checking). He spends most of his time developing the CodeContracts static checker, a static verifier based on abstract interpretation. Before joining MSR, Francesco was a post-doctoral student at the ENS, France, with Prof. Cousot, and a Ph.D. student at Ecole Polytechnique, France, with Dr. Radhia Cousot. He published papers in the most prestigious venues (e.g., POPL, OOPSLA, VMCAI, and SAS) and he was co-chair of SAS and VMCAI. In his spare time, Francesco enjoys his family and riding his road bike (he is an avid cyclist).
Ricky E. "Ranger" Sward is a Lead Information Systems Engineer for the MITRE Corporation in Colorado Springs, CO, USA. He currently supports a project to develop data and video collaboration widgets for the Army's DCGS-A system. He is also supporting an internal MITRE research project on 3D printed Unmanned Aircraft Systems and Android control of robots. Ranger retired from the US Air Force in August 2006 after a 21 year career as a Communications and Computer officer. He taught at the US Air Force Academy for 10 years where he taught courses such as Software Engineering and Unmanned Aircraft Systems. He has a B.S. and an M.S. in Computer Science, as well as a Ph.D. in Computer Engineering.
He is currently Past Chair of ACM SIGAda.
He can be reached via email at rsward at mitre.org
S. Tucker Taft has been involved with language design and implementation for over thirty years. Mr. Taft has been a member of teams implementing various compilers and real-time kernels since 1981. From 1990 to 1995 Mr. Taft was the lead technical designer of Ada 95, and since then has been active in the designs of Ada 2005 and Ada 2012. Most recently Mr. Taft has designed a new parallel programming language known as ParaSail, for "Parallel Specification and Implementation Language." The design and implementation of ParaSail over the past three years has been chronicled in a blog:
He can be reached via email at taft at adacore.com