Related Research Articles
In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics without performing all the calculations.
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.
The Message Passing Interface (MPI) is a standardized and portable message-passing standard designed to function on parallel computing architectures. The MPI standard defines the syntax and semantics of library routines that are useful to a wide range of users writing portable message-passing programs in C, C++, and Fortran. There are several open-source MPI implementations, which fostered the development of a parallel software industry, and encouraged development of portable and scalable large-scale parallel applications.
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.
In computer science, symbolic execution (also symbolic evaluation or symbex) is a means of analyzing a program to determine what inputs cause each part of a program to execute. An interpreter follows the program, assuming symbolic values for inputs rather than obtaining actual inputs as normal execution of the program would. It thus arrives at expressions in terms of those symbols for expressions and variables in the program, and constraints in terms of those symbols for the possible outcomes of each conditional branch. Finally, the possible inputs that trigger a branch can be determined by solving the constraints.
Model-based testing is an application of model-based design for designing and optionally also executing artifacts to perform software testing or system testing. Models can be used to represent the desired behavior of a system under test (SUT), or to represent testing strategies and a test environment. The picture on the right depicts the former approach.
In computer science, partial order reduction is a technique for reducing the size of the state-space to be searched by a model checking or automated planning and scheduling algorithm. It exploits the commutativity of concurrently executed transitions that result in the same state when executed in different orders.
The Portable, Extensible Toolkit for Scientific Computation, is a suite of data structures and routines developed by Argonne National Laboratory for the scalable (parallel) solution of scientific applications modeled by partial differential equations. It employs the Message Passing Interface (MPI) standard for all message-passing communication. PETSc is the world’s most widely used parallel numerical software library for partial differential equations and sparse matrix computations. PETSc received an R&D 100 Award in 2009. The PETSc Core Development Group won the SIAM/ACM Prize in Computational Science and Engineering for 2015.
The Parallel Virtual File System (PVFS) is an open-source parallel file system. A parallel file system is a type of distributed file system that distributes file data across multiple servers and provides for concurrent access by multiple tasks of a parallel application. PVFS was designed for use in large scale cluster computing. PVFS focuses on high performance access to large data sets. It consists of a server process and a client library, both of which are written entirely of user-level code. A Linux kernel module and pvfs-client process allow the file system to be mounted and used with standard utilities. The client library provides for high performance access via the message passing interface (MPI). PVFS is being jointly developed between The Parallel Architecture Research Laboratory at Clemson University and the Mathematics and Computer Science Division at Argonne National Laboratory, and the Ohio Supercomputer Center. PVFS development has been funded by NASA Goddard Space Flight Center, The DOE Office of Science Advanced Scientific Computing Research program, NSF PACI and HECURA programs, and other government and private agencies. PVFS is now known as OrangeFS in its newest development branch.
The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.
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.
A computer cluster is a set of computers that work together so that they can be viewed as a single system. Unlike grid computers, computer clusters have each node set to perform the same task, controlled and scheduled by software. The newest manifestation of cluster computing is cloud computing.
William Douglas Gropp is the director of the National Center for Supercomputing Applications (NCSA) and the Thomas M. Siebel Chair in the Department of Computer Science at the University of Illinois at Urbana–Champaign. He is also the founding Director of the Parallel Computing Institute. Gropp helped to create the Message Passing Interface, also known as MPI, and the Portable, Extensible Toolkit for Scientific Computation, also known as PETSc.
Concolic testing is a hybrid software verification technique that performs symbolic execution, a classical technique that treats program variables as symbolic variables, along a concrete execution path. Symbolic execution is used in conjunction with an automated theorem prover or constraint solver based on constraint logic programming to generate new concrete inputs with the aim of maximizing code coverage. Its main focus is finding bugs in real-world software, rather than demonstrating program correctness.
In computing, algorithmic skeletons, or parallelism patterns, are a high-level parallel programming model for parallel and distributed computing.
Róbert Lovas is a Hungarian computer scientist at SZTAKI, Budapest, Hungary.
Message passing is an inherent element of all computer clusters. All computer clusters, ranging from homemade Beowulfs to some of the fastest supercomputers in the world, rely on message passing to coordinate the activities of the many nodes they encompass. Message passing in computer clusters built with commodity servers and switches is used by virtually every internet service.
David Lansing Dill is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and computational systems biology.
Kenneth L. McMillan is an American computer scientist working in the area of formal methods, logic, and programming languages. He is a professor in the computer science department at the University of Texas at Austin, where he holds the Admiral B.R. Inman Centennial Chair in Computing Theory.
References
- ↑ Patrice Godefroid, Model Checking for Programming Languages using VeriSoft POPL 1997
- ↑ Cormac Flanagan and Patrice Godefroid, Dynamic partial-order reduction for model checking software,, POPL 2005, pp. 110-121, ACM, ISBN 1-58113-830-X
- ↑ Sarvani Vakkalanka, Ganesh Gopalakrishnan, and Robert M. Kirby, Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings, Computer Aided Verification (CAV 2008), pp. 66-79, LNCS 5123.
Anh Vo, Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, and Rajeev Thakur, Formal Verification of Practical MPI Programs, PPoPP 2009
Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, and Robert M. Kirby, Scheduling Considerations for Building Dynamic Verification Tools for MPI, Parallel and Distributed Systems - Testing and Debugging (PADTAD-VI) Archived 2008-09-30 at the Wayback Machine , Seattle, WA, July, 2008.
Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, Implementing Efficient Dynamic Formal Verification Methods for MPI Programs, Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/MPI 2008), Dublin, Ireland, 2008, LNCS 5205, pp. 248–256.
Sarvani Vakkalanka, Subodh Sharma, Ganesh Gopalakrishnan, and Robert M. Kirby, ISP: A Tool for Model Checking MPI Programs, Principles and Practices of Parallel Programming (PPoPP 2008) Archived 2009-02-08 at the Wayback Machine , Salt Lake City, February 2008, pp. 285–286.
Salman Pervez, Robert Palmer, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, Practical Model Checking Methods for Verifying Correctness of MPI Programs, Recent Advances in Parallel Virtual Machine and Message Passing Interface (PDF) Archived 2008-04-18 at the Wayback Machine (EuroPVM/MPI), Paris, 344—353, LNCS 4757, France, September 30 - October 3, 2007