In computer science, static program analysis is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution in the integrated environment.
In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.
The National Institute for Research in Digital Science and Technology (Inria) is a French national research institution focusing on computer science and applied mathematics. It was created under the name French Institute for Research in Computer Science and Automation (IRIA) in 1967 at Rocquencourt near Paris, part of Plan Calcul. Its first site was the historical premises of SHAPE, which is still used as Inria's main headquarters. In 1980, IRIA became INRIA. Since 2011, it has been styled Inria.
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.
UPPAAL is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types.
A synchronous programming language is a computer programming language optimized for programming reactive systems.
In computer science, an abstract state machine (ASM) is a state machine operating on states that are arbitrary data structures.
The Max Planck Institute for Software Systems (MPI-SWS) is a computer science research institute co-located in Saarbrücken and Kaiserslautern, Germany. The institute is chartered to conduct basic research in all areas related to the design, analysis, modelling, implementation and evaluation of complex software systems. Particular areas of interest include programming systems, distributed and networked systems, embedded and autonomous systems, as well as crosscutting aspects like formal modelling and analysis of software systems, security, dependability and software engineering. It joins over 80 other institutes run by the Max-Planck-Gesellschaft, which conduct world-class basic research in medicine, biology, chemistry, physics, technology and the humanities.
Gernot Heiser is a Scientia Professor and the John Lions Chair for operating systems at UNSW Sydney, where he leads the Trustworthy Systems group (TS).
The Advanced Learning and Research Institute (ALaRI), a faculty of informatics, was established in 1999 at the University of Lugano to promote research and education in embedded systems. The Faculty of Informatics within very few years has become one of the Switzerland major destinations for teaching and research, ranking third after the two Federal Institutes of Technology, Zurich and Lausanne.
Rajeev Alur is an American professor of computer science at the University of Pennsylvania who has made contributions to formal methods, programming languages, and automata theory, including notably the introduction of timed automata and nested words.
Joseph Sifakis is a Greek-French computer scientist. He received the 2007 Turing Award, along with Edmund M. Clarke and E. Allen Emerson, for his work on model checking.
OpenComRTOS is a commercial network-centric, formally developed real-time operating system (RTOS), aimed mainly at the embedded system market.
SIGNAL is a programming language based on synchronized data-flow : a process is a set of equations on elementary flows describing both data and control.
TAPAAL is a tool for modelling, simulation and verification of Timed-Arc Petri nets developed at Department of Computer Science at Aalborg University in Denmark and it is available for Linux, Windows and Mac OS X platforms.
PragmaDev Studio is a modeling and testing software tool introduced by PragmaDev in 2002 dedicated to the specification of communicating systems. It was initially called Real Time Developer Studio or RTDS. Its primary objective was to support SDL-RT modeling technology. Since V5.0 launched on October 7, 2015 RTDS is called PragmaDev Studio, and it is organized in four independent modules: Specifier, Developer, Tester and Tracer. V5.1 launched on November 29, 2016 introduces a freemium licensing model.
Harmony is an experimental computer operating system (OS) developed at the National Research Council Canada in Ottawa. It is a second-generation message passing system that was also used as the basis for several research projects, including robotics sensing and graphical workstation development. Harmony was actively developed throughout the 1980s and into the mid-1990s.
Kim Guldstrand Larsen R is a Danish scientist and professor of computer science at Aalborg University, Denmark. His field of research includes modeling, validation and verification, performance analysis, and synthesing of real-time, embedded, and cyber-physical systems utilizing and contributing to concurrency theory and model checking. Within this domain, he has been instrumental in the invention and continuous development of one of the most widely used verification tools, and has received several awards and honors for his work.
