Our research
Content type
+
Downloads (421)
+
Events (355)
 
Groups (147)
+
News (2467)
 
People (825)
 
Projects (1015)
+
Publications (11430)
+
Videos (4861)
Labs
Research areas
Algorithms and theory47205 (2)
Communication and collaboration47188 (6)
Computational linguistics47189 (13)
Computational sciences47190 (21)
Computer systems and networking47191 (25)
Computer vision208594 (0)
Data mining and data management208595 (0)
Economics and computation47192 (0)
Education47193 (2)
Gaming47194 (1)
Graphics and multimedia47195 (17)
Hardware and devices47196 (8)
Health and well-being47197 (13)
Human-computer interaction47198 (21)
Machine learning and intelligence47200 (14)
Mobile computing208596 (0)
Quantum computing208597 (0)
Search, information retrieval, and knowledge management47199 (22)
Security and privacy47202 (9)
Social media208598 (0)
Social sciences47203 (2)
Software development, programming principles, tools, and languages47204 (26)
Speech recognition, synthesis, and dialog systems208599 (0)
Technology for emerging markets208600 (0)
1–25 of 26
Sort
Show 25 | 50 | 100
12Next 
F* extends core-ML with a type system based on dependent refinements, higher kinds and affine types. It enables verification of higher-order stateful programs with automation via SMT solving.
Details
Date: 2 September 2013
Version: 0.7.1-alpha
Size: 35.50 MB
Type: Download
Implementation of algorithms to sample software projects for empirical research. The implementation is provided as an R package and provides two functions: (1) Score a selection of software projects (sample) with respect to how representative it is of a broader population. (2) Recommend additional projects from the broader population in order to maximize the score from the previous step.
Details
Date: 18 June 2013
Version: 0.1.1
Size: 0.01 MB
Type: Download
With this tool kit, users can mine linear temporal rules involving multiple events. The mined rules can capture data constraints on event fields and data-flow constraints between event fields via quantification. The tool kit can be used to mine rules over different views of events using event abstractions. In addition, the tool kit can be used to mine non-temporal rules involving single events, similar to frequent item sets. The tools operate on a well-defined, publicly available custom XML trace format....
Details
Date: 17 June 2013
Version: 5.0
Size: 0.54 MB
Type: Download
SymDiff, a language-agnostic tool for equivalence checking and displaying semantic (behavioral) differences over imperative programs. The tool operates at the level of the intermediate verification language Boogie, and hence language-agnostic. This download contains a front end for comparing C programs compiled using the Microsoft C compiler.
Details
Date: 26 December 2012
Version: 1.1
Size: 44.12 MB
Type: Download
With the Project Hawaii software-development kit for the Android operating system, you can develop Android applications that take advantage of cloud services and Windows Azure for computation and data storage. Project Hawaii provides the tools and services; you provide the creativity and imagination.
Details
Date: 20 September 2012
Version: 2.1
Size: 1.80 MB
Type: Download
With the Project Hawaii software-development kit for Windows 8, you can develop Windows Store apps that take advantage of cloud services and Windows Azure for computation and data storage. Project Hawaii provides the tools and services; you provide the creativity and imagination.
Details
Date: 12 September 2012
Version: 2.1
Size: 3.19 MB
Type: Download
Concurrency Sleuth is a property checker for concurrent programs. It uses efficient, language-independent techniques to search the set of behaviors of a program for bugs. Currently, it supports only programs written in the C programming language.
Details
Date: 28 August 2012
Version: 1.1
Size: 8.44 MB
Type: Download
Holmes is an automated debugging and failure-analysis tool that uses statistical analysis of code-coverage data to identify the most likely cause of test failures. Holmes uses a custom data-collection tool to amass detailed path coverage during testing. The tool analyzes this coverage data to find paths that strongly correlate with failure. Holmes can be used to select and analyze a set of test runs, to navigate to the most likely causes of test failures in source code, to set break points, and to re-run...
Details
Date: 1 December 2011
Version: 1.2.0.2
Size: 6.00 MB
Type: Download
Automata is a .NET tool kit that provides facilities for manipulating and analyzing regular expressions, symbolic finite automata, and symbolic finite transducers. It supports automata and transducers where input and output alphabets can be fully symbolic. Constraints over the alphabets can be analyzed using Satisfiability Modulo Theory (SMT) solvers. The tool kit provides a particular extension that uses the Microsoft SMT solver Z3.
Details
Date: 27 October 2011
Version: 1.0.0.0
Size: 3.13 MB
Type: Download
Memoir is a framework for building trusted modules with state continuity. The framework is described in our paper, Memoir: Practical State Continuity for Protected Modules.
Details
Date: 5 April 2011
Version: 1.0.0
Size: 0.18 MB
Type: Download
This Visual Studio Add-in and bare-metal environment enables the development of bare-metal applications for the Intel Single-chip Cloud Computer (SCC) research platform.
Details
Date: 27 March 2011
Version: 1.2
Size: 2.09 MB
Type: Download
This package contains the F# and F7 source files to aid in the verification of a distributed key-management system. This new component implements a data-protection API for groups of clients. To enable long-term data protection, it supports cryptographic agility so cryptography algorithms and policies can evolve for protecting fresh data while preserving access to old data. To verify the security of our design and production code, written in C#, we write a reference implementation in F#. Formally, we verify...
Details
Date: 2 December 2010
Version: 1.2.0
Size: 0.03 MB
Type: Download
Holmes is an automated debugging and failure-analysis tool that uses statistical analysis of code-coverage data to identify the most likely cause of test failures. Holmes uses a custom data-collection tool to amass detailed path coverage during testing. The tool analyzes this coverage data to find paths that strongly correlate with failure. Holmes integrates seamlessly with all test workflows in Visual Studio. Developers can use Holmes to select and analyze a set of test runs, to navigate to the most...
Details
Date: 23 November 2010
Version: 1.2.0.2 Beta
Size: 6.50 MB
Type: Download
This tool finds data races in multithreaded code. It uses a combination of code and data break points to find data races effectively with little or no runtime overhead.
Details
Date: 19 October 2010
Version: 1.0.0
Size: 0.57 MB
Type: Download
Pex (Program EXploration) is a white-box test generation tool. Given a hand-written parameterized unit test, Pex analyzes the code to determine relevant test inputs fully automatically. The result is a traditional unit test suite with high code coverage.
Details
Date: 12 October 2010
Version: 0.94.51006.1
Size: 15.56 MB
Type: Download
Guesstimate is a programming model for developing collaborative distributed applications. The goal of Guesstimate is to provide a simple, object-oriented model for developing distributed-systems applications. The programming model is exposed as a C# API. The API enables programmers to develop distributed-systems applications in an object-oriented manner. API methods are provided to create new distributed-systems objects, to subscribe to existing objects, and to issue operations to change the state of the...
Details
Date: 10 August 2010
Version: 1.0
Size: 0.80 MB
Type: Download
This is a source release of the Fine compiler and several example programs. The Fine compiler implements a type system that enables the enforcement of rich, stateful authorization and information-flow policies to be verified. Our compilation technique produces verifiable target code in a language called DCIL, an extension of CIL, the language of the .NET runtime. Code consumers can check DCIL target programs using a syntactic byte-code verifier to establish the security of the code.
Details
Date: 28 May 2010
Version: 0.3-alpha
Size: 4.92 MB
Type: Download
This tool enables biologists and modelers to construct high-level theories and models of biological systems, capturing biological hypotheses, inferred mechanisms, and experimental results within the same framework. The main components of the tool are a visual editor for constructing the model and to visualize the dynamic behavior, and an execution and analysis engine that can run the models in batch mode, interactive mode, or deterministic versus nondeterministic modes. During runtime, the execution engine...
Details
Date: 17 May 2010
Version: 1.0.0.0
Size: 0.97 MB
Type: Download
This is a compiler for the Bulk-Synchronous GPU Programming (BSGP) language. BSGP is a new language for general-purpose computation on a graphics processing unit (GPU). BSGP programs look similar to sequential C programs, and programmers need to supply only a bare minimum of extra information to describe parallel processing on GPUs. As a result, BSGP programs are easy to read, write, and maintain, and the ease of programming does not come at the cost of performance.
Details
Date: 12 December 2009
Version: 2.0.0.2
Size: 38.40 MB
Type: Download
Dryad is a high-performance, general-purpose, distributed-computing engine that simplifies the task of implementing distributed applications on clusters of computers running a Windows® operating system. DryadLINQ enables developers to implement Dryad applications in managed code by using an extended version of the LINQ programming model and API. The academic release of Dryad and DryadLINQ provides the software necessary to develop DryadLINQ applications and to run them on a Windows HPC Server 2008 cluster....
Details
Date: 17 November 2009
Version: 1.0.1411.2
Size: 27.59 MB
Type: Download
Distribution for the standalone Subpolyhedra library, a new numerical abstract domain for scalable inference and propagation of linear inequalities.
Details
Date: 10 October 2008
Version: 0.1
Size: 0.48 MB
Type: Download
The PSL-to-Verilog compiler (P2V) generates hardware checkers for assertions made on a software program, using the Property Specification Language (PSL). The compiler is written in Python and compiles for the eMIPS dynamically extensible processor.
Details
Date: 27 August 2008
Version: 1.0
Size: 0.62 MB
Type: Download
HAVOC is a modular verifier for systems software written in C. It takes as input an annotated C program, in the form of pre- and post-conditions and loop invariants, and uses the Boogie verifier and the SMT solver Z3 to check the annotations. The novelty of the tool lies in a) an accurate memory model for C accounting for low-level operations such as pointer arithmetic, address-of operations, and casts; b) an expressive annotation language; and c) efficient decision procedures to reason about the...
Details
Date: 2 June 2008
Version: 0.1
Size: 9.57 MB
Type: Download
FS2PV is a verification tool that compiles cryptographic-protocol implementations in a first-order subset of F# to a formal pi-calculus model. This pi-calculus model then can be analyzed using ProVerif to prove the desired security properties or to find security flaws.
Details
Date: 14 February 2007
Version: 1.0
Size: 2.19 MB
Type: Download
Abstract IL an SDK for manipulating .NET Framework files and binaries. You can use this release from any .NET programming language, though it is best used from F#, or the OCaml language. With it you can access the contents of .NET binaries at a high-level, avoiding the details of the binary format. Abstract IL has been used for a compiler (F#), a static analysis tool looking analyzing code access security and an aspect-oriented programming project.
Details
Date: 20 September 2006
Version: 1.1.12.5
Size: 8.24 MB
Type: Download
1–25 of 26
Sort
Show 25 | 50 | 100
12Next 
> Our research