High Integrity Language Technology
ACM SIGAda’s Annual International Conference
Jason Belt is a Ph.D. Candidate at the Computing and Information Sciences (CIS) Department at Kansas State University (KSU). He received his M.S. from KSU CIS and his research focuses on software verification and analysis. For his Ph.D. work, he develops Bakar Kiasan -- a symbolic execution, evidence-based program verification tool targeting Spark Ada.
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 Jeff at Boleng.Com
Dr. Patrice Chalin is an Associate Professor at KSU CIS who has been doing research in specification and programming language semantics as well as program verification since the early 90s. He has also been active in the development of verification tooling including JmlEclipse, an IDE for Java supporting the Java Modeling Language. More recent efforts in language design, semantics, tooling and tutorials have come to focus on Spark/Ada and its symbolic execution.
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).
Cody Fleming is pursuing a doctoral degree in the aeronautics and astronautics at the Massachusetts Institute of Technology. He holds a BS degree in mechanical engineering from Hope College and masters in civil engineering from MIT. Prior to returning to MIT, he spent 5 years working in space system development for various government projects.
Dr. John Hatcliff is a University Distinguished Professor at KSU CIS. Hatcliff’s research focuses on developing software design and verification tools for embedded security systems and integrated medical systems. He has been Principal Investigator on a number of Department of Defense research grants focusing on safety-critical software. He is a co-recipient of a 2010 International Conference on Software Engineering (ICSE) Most Influential Paper (MIP) award and 2010 ACM Special Interest Group on Software Engineering (SIGSOFT) Impact award; these awards are typically given to a research paper that is deemed to make the most significant contribution to software engineering theory and practice a decade after the paper is originally published.
Johannes Kanig holds engineering degrees of the Ecole Centrale Paris, France and the Technical University of Dresden, Germany. He has done his PhD in formal methods at the french research institute INRIA near Paris. Johannes is Software engineer and works on the static analysis tools developed at AdaCore, namely CodePeer and GNATprove.
Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research. He is known for his work on programming methods and program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3. With Dafny, his mission is not just to provide a tool that helps teach programmers to reason about programs, but also to provide a vision for the kind of automatic reasoning support that all future programming environments may provide.
Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner video show on channel9.msdn.com. In his spare time, he plays music and, recently having ended his tenure as cardio exercise class instructor, is trying to learn to dance.
Nancy Leveson is Professor of Aeronautics and Astronautics and also Engineering Systems at Massachusetts Institute of Technology. She is an elected member of the National Academy of Engineering. Professor Leveson conducts research on the topics of system safety, software safety, software and system engineering, and human-computer interaction. In 1999, she received the ACM Allen Newell Award for outstanding computer science research and in 1995 the AIAA Information Systems Award for “developing the field of software safety and for promoting responsible software and system engineering practices where life and property are at stake.” In 2005 she received the ACM Sigsoft Outstanding Research Award. She has published over 200 research papers and is author of two books, "Safeware: System Safety and Computers" published by Addison-Wesley, and “Engineering a Safer World”, published by MIT Press in 2012. She consults extensively in many industries on the ways to prevent accidents.
Dr. Kelvin Nilsen is Chief Technology Officer over Java at Atego Systems, a mission- and safety-critical solutions provider, where he oversees the design and implementation of the Perc virtual machine and other Atego embedded/real-time oriented products. Prior to joining Atego, Dr. Nilsen served on the faculty of Iowa State University where he performed seminal research on real-time Java that led to the Perc family of virtual machine products. He is the original architect of the Perc Ultra virtual machine and the Perc Pico hard real-time technology. Dr. Nilsen actively participates in the Java Community Process as a member of the JSR 282 and JSR 302 expert groups. He holds a B.S. in Physics and M.S. and Ph.D. degrees in Computer Science.
Dr. Robby is an Associate Professor at KSU CIS. His main research interests are in the area of software specification and verification techniques. He received a NSF CAREER award in 2007 for his work on formal software analysis for open systems, which has resulted in the development of the highly automated Kiasan symbolic execution-based program verification framework that is applicable to various application domains and software artifact level of abstractions such as software model, specification, and code. He is also a co-recipient of the 2010 ICSE MIP and the 2010 ACM SIGSOFT Impact awards.
Dr. Bo Sandén began his career as a software developer in industry and had the opportunity to study and design multithreaded software. 1986-87 he was a Visiting Associate Professor in the pioneering software-engineering program at the Wang Institute, Tyngsboro, MA. As an Associate Professor at George Mason University, Fairfax, VA 1987-1996, he helped create a master’s program in software systems engineering and taught design and led capstone projects with a focus on concurrent software. Since 1996 he is a Professor of Computer Science at Colorado Technical University in Colorado Springs, where he has taught at the undergraduate and master’s levels and now exclusively teaches and directs student research in the Doctor of Computer Science program.
Dr. Sandén is the inventor of entity-life modeling and the author of “Design of multithreaded software: The entity-life modeling approach.” He gave a number of tutorials on ELM in the mid-90s: ACM Professional Development Seminar 1994, Washington Ada Symposium 1994, 1995, 1996; TRI-Ada 1994, 1995, 1996. Since then he has taught ELM at Colorado Tech and externally, and published a number of articles on the topic primarily in the IEEE magazines. His tutorial on ELM at Ada Europe 2012 was well attended.
Ricky E. "Ranger" Sward is a Lead Information Systems Engineer for the MITRE Corporation in Colorado Springs, CO, USA. He currently supports the Air Force A2U Unmanned Systems ISR Innovations Branch working to integrate full-motion video initiatives for unmanned aircraft systems. He is also supporting an internal MITRE research project on composable widgets using a Service Oriented Architecture (SOA) implementation. Ranger retired from the 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 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
John Thomas is pursuing a doctoral degree in the Engineering Systems Division at the Massachusetts Institute of Technology. Prior to beginning his doctoral studies, he spent four years working on various Department of Defense projects, specializing in system engineering and requirements development. He holds BS and MS degrees in Computer Engineering, both from the University of Massachusetts.