-
SAT 20222022We present approaches to store and restore the state of a SAT solver, allowing us to migrate the state between different compute resources, or even between different solvers. This can be used in many ways, e.g., to improve the fault tolerance of solvers, to schedule SAT problems on a restricted number of cores, or to use dedicated preprocessing tools for in-processing. We identify a minimum viable subset
-
ISSTA 20222022Verification toolchains are widely used to prove the correctness of critical software systems. To build confidence in their results, it is important to develop testing frameworks that help detect bugs in these toolchains. Inspired by the success of fuzzing in finding bugs in compilers and SMT solvers, we have built the first fuzzing and differential testing framework for Dafny, a high-level programming
-
PLDI 20222022We present a novel approach to differential cost analysis that, given a program revision, attempts to statically bound the difference in resource usage, or cost, between the two program versions. Differential cost analysis is particularly interesting because of the many compelling applications for it, such as detecting resource-use regressions at code-review time or proving the absence of certain side-channel
-
TACAS 20222022Dafny is a verifcation-aware programming language used at Amazon Web Services to develop critical components of their access management, storage, and cryptography infrastructures. The Dafny toolchain provides a verifer that can prove an implementation of a method satisfies its specification. When the underlying SMT solver cannot establish a proof, it generates a counterexample. These counterexamples are
-
2021Integrating static analyses into continuous integration (CI) or continuous delivery (CD) has become the best practice for assuring code quality and security. Static Application Security Testing (SAST) tools fit well into CI/CD, because CI/CD allows time for deep static analyses on large code bases and prevents vulnerabilities in the early stages of the development lifecycle. In CI/CD, the SAST tools usually
Related content
-
March 08, 2023This year’s cohort is researching, among other topics, online changepoint detection algorithms and automated reasoning.
-
September 29, 2022Majumdar’s 2003 paper established an elegant algorithm that influences current work on timed games.
-
September 21, 2022Scientists’ paper on probabilistic symbolic execution has significantly influenced software testing and analysis.
-
August 18, 2022CAV keynote lecture by the director of applied science for AWS Identity explains how AWS is making the power of automated reasoning available to all customers.
-
August 08, 2022To mark the occasion of the eighth Federated Logic Conference (FloC), Amazon’s Byron Cook, Daniel Kröning, and Marijn Heule discussed automated reasoning’s prospects.
-
July 15, 2022Hicks wins 2022 ACM SIGPLAN Distinguished Service Award for career contributions; Vidal wins IEEE Signal Processing Magazine Best Paper Award.
-
June 17, 2022Automated-reasoning method enables the calculation of tight bounds on the use of resources — such as computation or memory — that results from code changes.
-
February 14, 2022Jhala received the ACM honor for lifetime contributions to software verification, developing innovative tools to help computer programmers test their code.
-
February 10, 2022Distributing proof search, reasoning about distributed systems, and automating regulatory compliance are just three fruitful research areas.
-
December 01, 2021Meet Amazon Science’s newest research area.
-
November 30, 2021Submission period extends from December 6, 2021 to January 21, 2022.
-
November 02, 2021SOSP paper describes lightweight formal methods for validating new S3 data storage service.
-
September 07, 2021The 26 awardees represent 25 universities in 11 countries. Recipients have access to more than 250 Amazon public datasets, and can utilize AWS AI/ML services and tools.
-
July 29, 2021Amazon’s Dan Roth on a hot new research topic — that he’s been studying for more than 25 years.
-
April 19, 2021In a pilot study, an automated code checker found about 100 possible errors, 80% of which turned out to require correction.
-
March 18, 2021Submission period extends from March 22 to April 23, 2021.
-
October 27, 2020Rungta had a promising career with NASA, but decided the stars aligned for her at Amazon.
-
August 19, 2020Amazon engineers discuss networking advances and challenges in virtual session at SIGCOMM 2020.
-
July 24, 2020Amazon automated reasoning scientists showcase verification methods being applied across Amazon during CAV 2020.
-
June 24, 2020Amazon scientists are on the cutting edge of using math-based logic to provide better network security, access management, and greater reliability.