For Statemate, the first embodiment in a commercial computer-aided software engineering tool of a rigorous approach to model-driven development based on statecharts, and employing techniques for the executability of visual formalisms, and for code-generation.
ABOUT THIS AWARD
Awarded to an institution or individual(s) recognized for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. The Software System Award carries a prize of $35,000. Financial support for the Software System Award is provided by IBM.
Coq selected as recipient of the 2013 Software system Award
Coq is a software tool for the interactive development of formal proofs, which is a key enabling technology for certified software. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. An open source product, Coq has played an influential role in formal methods, programming languages, program verification and formal mathematics. As certification gains importance in academic and industrial arenas, Coq plays a critical role as a primary programming and certification tool. Coq’s first implementation was in 1985, when it was named CoC (the acronym for the logic it implemented: the Calculus of Constructions). This system was developed by the Coq Development Team whose primary members were Thierry Coquand, University of Gothenburg; Gérard Huet, INRIA Paris - Rocquencourt; Christine Paulin-Mohring, University Paris Sud/INRIA Saclay; Bruno Barras, INRIA Saclay/École Polytechnique; Jean-Christophe Filliâtre, CNRS/INRIA Saclay; Hugo Herbelin, INRIA Paris - Rocquencourt; Chet Murthy, Google Inc.; Yves Bertot, INRIA Sophia; and Pierre Castéran, University of Bordeaux.
ACM will present the 2013 Software System Award at its annual Awards Banquet on June 21 in San Francisco, CA.
Adve, Cheng, Lattner recipients of the 2012 Software System Award
LLVM is a language-independent collection of programming technologies that enables code analysis and transformation for arbitrary programming languages. A collection of compiler technologies that turn programming languages into machine code used by processors, LLVM is widely used in commercial products as well as computer science research. Key factors in its success are the openness of its technology and the quality of its architecture and engineering as well as its clean, flexible design and easy-to-use programming interfaces.
The LLVM project started in 2000 at the University of Illinois at Urbana-Champaign (UIUC) under the direction of Chris Lattner (now director of Developer Tools at Apple) and Vikram Adve, a professor at UIUC. Evan Cheng drove the design and implementation of the code generator in LLVM, and is now a senior manager at Apple. In the years since its release, LLVM has been incorporated into commercial products by Apple, Adobe, AMD, Arxan, AutoESL, Cray, Google, Intel, and many others.
