-
ICSE 20232023Static application security testing (SAST) tools have found broad adoption in modern software development workflows. These tools employ a variety of static analysis rules to generate recommendations on how to improve the code of an application. Every recommendation consumes the time of the engineer that is investigating it, so it is important to measure how useful these rules are in the long term. But what
-
FM 20232023Computational notebooks are widely used for machine learning (ML). However, notebooks raise new correctness concerns beyond those found in traditional programming environments. ML library APIs are easy to misuse, and the notebook execution model raises entirely new problems concerning reproducibility. It is common to use static analyses to detect bugs and enforce best practices in software applications.
-
CAV 20222022Amazon Web Services (AWS) is a cloud computing services provider that has made significant investments in applying formal methods to proving correctness of its internal systems and providing assurance of correctness to their end-users. In this paper, we focus on how we built abstractions and eliminated specifications to scale a verification engine for AWS access policies, Zelkova, to be usable by all AWS
-
Reiner Hähnle Symposium2022This paper introduces a specification construct that is fitting when combining verified code with unverified code. The specification is a form of precondition that imposes proof obligations for both callers and callees. This precondition, recommends, blends in well with the parameter-validation conventions in Java and with the syntax and semantics of specification languages such as JML, ACSL, and Dafny.
-
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
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.