Social
Publication

Free facts: An alternative to inefficient axioms in Dafny

By Tabea Bordis, Rustan Leino
2024
Download Copy BibTeX
Share
Download
Copy BibTeX
Share
Abstract. Formal software verification relies on properties of functions and built-in operators. Unless these properties are handled directly by decision procedures, an automated verifier includes them in verification conditions by supplying them as universally quantified axioms or theorems. The use of quantifiers sometimes leads to bad performance, especially if automation causes the quantifiers to be instantiated many times. This paper proposes free facts as an alternative to some axioms. A free fact is a pre-instantiated axiom that is generated alongside the formulas in a verification condition that can benefit from the facts. Replacing an axiom with free facts thus reduces the number of quantifiers in verification conditions. Free facts are statically triggered by syntactic occurrences of certain patterns in the proof terms. This is less powerful than the dynamically triggered patterns used during proof construction. However, the paper shows that free facts perform well in practice.
Research areas
Tags

Latest news

Work with us

See more jobs See more jobs
Sr. Communication Systems Design Engineer, Wireless Systems
US, TX, Austin
Amazon Leo is an initiative to launch a constellation of Low Earth Orbit satellites that will provide low-latency, high-speed broadband connectivity to unserved and underserved communities around the world. As a Systems Engineer, this role is primarily responsible for the design, development and integration of Ka band and S/C band communication payload and ground terminal systems. The Role: Be part of the team defining the overall communication system and architecture of Amazon’s broadband wireless network. This is a unique opportunity to innovate and define groundbreaking wireless technology with few legacy constraints. The team develops and designs the communication system of Amazon Leo and analyzes its overall system level performance such as for overall throughput, latency, system availability, packet loss etc. This role in particular will be responsible for leading the effort in designing and developing advanced technology and solutions for communication system. This role will also be responsible developing advanced L1/L2 proof of concept HW/SW systems to improve the performance and reliability of the Amazon Leo network. In particular this role will be responsible for using concepts from digital signal processing, information theory, wireless communications to develop novel solutions for achieving ultra-high performance LEO network. This role will also be part of a team and develop simulation tools with particular emphasis on modeling the physical layer aspects such as advanced receiver modeling and abstraction, interference cancellation techniques, FEC abstraction models etc. This role will also play a critical role in the design, integration and verification of various HW and SW sub-systems as a part of system integration and link bring-up and verification. Export Control Requirement: Due to applicable export control laws and regulations, candidates must be a U.S. citizen or national, U.S. permanent resident (i.e., current Green Card holder), or lawfully admitted into the U.S. as a refugee or granted asylum. Key job responsibilities • Design advanced L1/L2 algorithms and solutions for the Amazon Leo communication system, particularly Multi-User MIMO techniques. • Develop proof-of-concepts for critical communication payload components using SDR platforms consisting of FPGAs and general-purpose processors. • Work with ASIC development teams to build power/area efficient L1/L2 HW accelerators to be integrated into Amazon Leo SoCs. • Provide specifications and work with implementation teams on the development of embedded L1/L2 HW/SW architectures. • Work with multi-disciplinary teams to develop advanced solutions for time, frequency and spatial acquisition/tracking in LEO systems, particularly under large uncertainties. • Develop link-level and system-level simulators and work closely with implementation teams to evaluate expected performance and provide quick feedback on potential improvements. • Develop testbeds consisting of digital, IF and RF components while accounting for link-budgets and RF/IF line-ups. Previous experiences with VSAs/VSGs, channel emulators, antennas (particularly phased-arrays) and anechoic chamber instrumentation are a plus. • Work with development teams on system integration and debugging from PHY to network layer, including interfacing with flight computer and SDN control subsystems. • Willing to work in fast-paced environment and take ownership that goes from algorithm specification, to HW/SW architecture definition, to proof-of-concept development, to testbed bring-up, to integration into the Amazon Leo system. • Be a team player and provide support when requested while being able to unblock themselves by reaching out to RF, ASIC, SW, Comsys and Testbed supporting teams to move forward in development, testing and integration activities. • Ability to adapt design and test activities based on current HW/SW capabilities delivered by the development teams.
Sr. Comm Systems Engineer, Wireless Systems
US, TX, Austin
Project Leo (former Kuiper) is an initiative to launch a constellation of Low Earth Orbit satellites that will provide low-latency, high-speed broadband connectivity to unserved and underserved communities around the world. As a Systems Engineer, this role is primarily responsible for the design, development and integration of Ka band and FR1 band communication payload and customer terminal systems. The Role: Be part of the team defining the overall communication system and architecture of Amazon Leo’s broadband wireless network. This is a unique opportunity to innovate and define groundbreaking wireless technology at global scale. The team develops and designs the communication system for project Leo and analyzes its overall system level performance such as for overall throughput, latency, system availability, packet loss etc. This role in particular will be responsible for leading the effort in designing and developing advanced technology and solutions for communication system. This role will also be responsible developing advanced physical layer + protocol stacks systems as proof of concept and reference implementation to improve the performance and reliability of the LEO network. In particular this role will be responsible for using concepts from digital signal processing, information theory, wireless communications to develop novel solutions for achieving ultra-high performance LEO network. This role will also be part of a team and develop simulation tools with particular emphasis on modeling the physical layer aspects such as advanced receiver modeling and abstraction, interference cancellation techniques, FEC abstraction models etc. This role will also play a critical role in the integration and verification of various HW and SW sub-systems as a part of system integration and link bring-up and verification. Export Control Requirement: Due to applicable export control laws and regulations, candidates must be a U.S. citizen or national, U.S. permanent resident (i.e., current Green Card holder), or lawfully admitted into the U.S. as a refugee or granted asylum.
Applied Scientist, Demand Forecasting
US, WA, Bellevue
What does it take to build a foundation model that can forecast demand for hundreds of millions of products — including ones that have never been sold before? At Amazon, our Demand Forecasting team is tackling one of the most ambitious challenges in applied time series research: designing and building large-scale foundation models that generalize across an enormous and diverse catalog of products, geographies, and business contexts. This is not incremental modeling work. We are redefining what's possible in demand forecasting through novel architectures, training strategies, and data generation techniques. Our team operates at a scale that is unmatched in industry or academia. You'll design experiments across millions of products simultaneously, developing new model architectures and training methodologies that push the boundaries of what foundation models can learn from vast, heterogeneous time series data. You'll explore techniques in transfer learning, zero-shot forecasting, and synthetic data generation. The models you design here will ship to production and directly influence hundreds of millions of dollars in automated inventory decisions every week. Beyond operational impact, you'll publish your work at top-tier conferences and contribute to advancing the state of the art in time series foundation models for the broader scientific community. If you are a scientist who wants to work at the frontier of time series research, design novel solutions to problems no one else has solved at this scale, and see your research deployed to real-world impact — this is the team for you. Key job responsibilities 1. Design and implement novel deep learning architectures (e.g., Transformers, SSMs, or Graph Neural Networks) for time-series foundation models that generalize across hundreds of millions of products and diverse global contexts. 2. Drive the full development cycle - from whiteboarding new algorithmic approaches to overseeing production-scale deployments. 3. Collaborate with SDEs to build high-performance, distributed training and inference pipelines; translate complex scientific concepts into scalable, production-grade code in Python and Scala. 4. Leverage and develop agentic GenAI workflows to automate the end-to-end research cycle from synthesizing state-of-the-art literature and auto-generating experimental code to rapidly iterating on model architectures across millions of products. 5. Maintain a high bar for scientific excellence by publishing novel research in top-tier venues (e.g., NeurIPS, ICLR, KDD) and contributing to Amazon’s internal patent and science community. A day in the life No two days look the same, but most will involve a high-velocity blend of deep architectural work, distributed system design, and frontier scientific thinking at a scale you won’t find anywhere else. You might start the morning by designing a synthetic data pipeline to stress-test your foundation model. You’ll use generative techniques to simulate rare "black swan" supply chain events, ensuring your model remains robust where historical data is thin. You'll then lead a Scientific Design Review, walking senior leaders through your model’s architecture, defending your choice of loss functions with data-driven rigor. You’ll write high-performance code often paired with AI-coding assistants to handle the heavy lifting of boilerplate and unit testing. You’ll collaborate across a "Two-Pizza Team" of scientists and engineers, pushing the boundaries of research with a clear goal: contributing to work that will be published at top-tier venues (ICLR, NeurIPS) while simultaneously driving multi-million dollar automated decisions. The work is hard, the math is complex, and the tools are state-of-the-art. If you want to build the models that actually ship—this is where you do it. About the team The Demand Forecasting team sits at the heart of Amazon's supply chain, building the science that determines what products are available, when, and at what cost — for hundreds of millions of customers around the world. Our mission is to push the frontier of what's possible in large-scale time series forecasting, and to deploy that science where it creates real, measurable impact. We are a team of scientists who care deeply about both research rigor and real-world outcomes. We don't just publish — we ship. And we don't just ship — we measure, iterate, and raise the bar. Our work spans the full lifecycle: from foundational research and large-scale experimentation to production deployment and downstream impact measurement across supply chain, inventory, and financial planning.
Research Scientist, Modeling and Optimization (MOP)
US, WA, Bellevue
Do you enjoy solving challenging problems and driving innovations in research? Are you seeking for an environment with a group of motivated and talented scientists like yourself? Do you want to create scalable optimization models and apply machine learning techniques to guide real-world decisions? Do you want to play a key role in the future of Amazon transportation and operations? Come and join us at Amazon's Modeling and Optimization team (MOP). Key job responsibilities A Research Scientist in the Modeling and Optimization (MOP) team - provides analytical decision support to Amazon planning teams via applying advanced mathematical and statistical techniques. - collaborates effectively with Amazon internal business customers, and is their trusted partner - is proactive and autonomous in discovering and resolving business pain-points within a given scope - is able to identify a suitable level of sophistication in resolving the different business needs - is confident in leveraging existing solutions to new problems where appropriate and is independent in designing and implementing new solutions where needed - is aware of the limitations of their proposed solutions and is proactive in communicating them to the business, and advances the application of sciences towards Amazon business problems by bringing new methods, ideas, and practices to the team and scientific community. A day in the life - Your will be developing model-based optimization, simulation, and/or predictive tools to identify and evaluate opportunities to improve customer experience, network speed, cost, and efficiency of capital investment. - You will quantify the improvements resulting from the application of these tools and you will evaluate the trade-offs between potentially competing objectives. - You will develop good communication skills and ability to speak at a level appropriate for the audience, will collaborate effectively with fellow scientists, software development engineers, and product managers, and will deliver business value in a close partnership with many stakeholders from operations, finance, IT, and business leadership. About the team - At the Modeling and Optimization (MOP) team, we use mathematical optimization, algorithm design, statistics, and machine learning to improve decision-making capabilities across WW Operations and Amazon Logistics. - We focus on transportation topology, labor and resource planning for fulfillment facilities, routing science, visualization research, data science and development, and process optimization. - We create models to simulate, optimize, and control the fulfillment network with the objective of reducing cost while improving speed and reliability. - We support multiple business lanes, therefore maintain a comprehensive and objective view, coordinating solutions across organizational lines where possible.
Economist III - AMZ9674161
US, NJ, Jersey City
MULTIPLE POSITIONS AVAILABLE Employer: AMAZON WEB SERVICES, INC. Offered Position: Economist III Job Location: Jersey City, New Jersey Job Number: AMZ9674161 Position Responsibilities: Work with the chief economist and senior management on key business problems faced in retail, international retail, cloud computing, third party merchants, search, Kindle, streaming video, or operations. Apply the frontier of economic thinking to market design, pricing, forecasting, program evaluation, online advertising, and other areas. Build econometric models using data systems. Apply economic theory to solve business problems. Develop new techniques to process large data sets, address quantitative problems, and contribute to design of automated systems. Apply tools from applied micro-econometrics (e.g. experimental design, difference-in-difference, regression discontinuity, and IV) and forecasting (essential time series models). Leverage big data tools for data extraction. Write up and present analysis for distribution to various levels of management at Amazon. Gain experience in academic research. Use program evaluation, forecasting, time series, panel data, and high dimensional problems. Use R and Stata. Position Requirements: Ph.D. or foreign equivalent degree in Economics, Finance, or a related field and three years of research or work experience in the job offered or a related occupation. Must have at least one year of research or work experience in the following skill(s): (1) working with Causal inference techniques (Difference-in-Differences, Matching, Double Machine Learning, Instrumental Variables, and Regression Discontinuity Designs); (2) statistical analysis tools (Python, R or Stata); (3) Data querying languages (SQL). Amazon.com is an Equal Opportunity-Affirmative Action Employer – Minority / Female / Disability / Veteran / Gender Identity / Sexual Orientation. 40 hours / week, 8:00am-5:00pm, Salary Range $175,100/year to $236,900/year. Amazon is a total compensation company. Dependent on the position offered, equity, sign-on payments, and other forms of compensation may be provided as part of a total compensation package, in addition to a full range of medical, financial, and/or other benefits. For more information, visit: https://www.aboutamazon.com/workplace/employee-benefits.#0000
Manager III, Economist - AMZ9782156
US, NY, New York
MULTIPLE POSITIONS AVAILABLE Employer: AMAZON.COM SERVICES LLC Offered Position: Manager III, Economist Job Location: New York, New York Job Number: AMZ9782156 Position Responsibilities: Support the measurement of the Alexa business and provide actionable insights across Alexa customers and devices. Work with product managers, SDEs, financial analysts, and BIEs to help the Alexa organization identify new features and business opportunities as well as drive optimization of current features and services through your analyses as the technical lead on the team. Own the development of econometric models, and manage the modelling and validation work for analysis products. Design and develop Econometric models to solve business problems and improve customer CX. Develop techniques to process large datasets, address quantitative problems, and contribute to design of automated systems around the company. Write high quality code and participating in Econ tech reviews, work with the business stakeholders to understand and solve their business problems by applying the frontier of economic thinking. Mentor and support junior Economists and scientists. Position Requirements: PhD degree or foreign equivalent in Economics, Computer Science, or related field and five years of research or work experience in the job offered or related occupation. Must have one year of research or work experience in the following skill(s): experience with casual inference and predictive modeling; experience in econometrics (program evaluation, forecasting, time series, panel data, and high dimensional problems); and experience with economic theory and quantitative methods. Amazon.com is an Equal Opportunity-Affirmative Action Employer – Minority / Female / Disability / Veteran / Gender Identity / Sexual Orientation. 40 hours / week, 8:00am-5:00pm, Salary Range $226,782/year to $260,500/year. Amazon is a total compensation company. Dependent on the position offered, equity, sign-on payments, and other forms of compensation may be provided as part of a total compensation package, in addition to a full range of medical, financial, and/or other benefits. For more information, visit: https://www.aboutamazon.com/workplace/employee-benefits.#0000
Data Scientist, SAMBA
US, NJ, Newark
At Audible, we believe stories have the power to transform lives. It’s why we work with some of the world’s leading creators to produce and share audio storytelling with our millions of global listeners. We are dreamers and inventors who come from a wide range of backgrounds and experiences to empower and inspire each other. Imagine your future with us. ABOUT THIS ROLE We are seeking a Data Scientist to own our causal inference infrastructure and drive sophisticated modeling that measures the incremental impact of business decisions. This role requires deep expertise in advanced causal inference methodologies—including synthetic control methods, Synthetic Difference-in-Differences (SDID), and Bayesian approaches—to design rigorous experiments, estimate long-term customer behavior effects, and translate complex analytical results into clear business recommendations. You will own the development and continuous improvement of these causal inference models while being responsible for machine learning operations at scale to ensure our organization makes data-driven decisions with confidence. At Audible, you will have an opportunity to make the best of your skillsets to both develop advanced scientific solutions and drive critical customer and business impact. You will play a key role to drive end-to-end solutions from understanding our business and business requirements, identifying opportunities from a large amount of historical data and engaging in research to solve the business problems. You'll seek to create value for both stakeholders and customers and inform findings in a clear, actionable way to managers and senior leaders. You will be at the heart of an agile and growing area at Audible. ABOUT THE TEAM Audible Data Scientists are members of a global interdisciplinary insights and research team with an integral role in the design and integration of models to automate decision making throughout the business in every country. We empower the machine learning and deep learning techniques in many areas of the business. We translate business goals into agile, insightful analytics and seek to create value for both stakeholders and customers and convey findings in a clear, actionable way to managers and senior leaders. As a Data Scientist, you will... - Design and execute geo-level randomized experiments to measure incremental impact - Apply statistical techniques to evaluate causal impact in quasi-experimental settings - Ensure experiments are statistically valid by evaluating sampling strategies, statistical power, and potential sources of bias - Develop models that estimate long-term effects from short-term experiments using machine learning - Estimate how changes in customer behavior persist and decay over time - Own and maintain the geo-testing codebase, including deployment and scalability - Implement machine learning models at scale with focus on performance optimization - Partner with stakeholders to ensure models align with real business dynamics - Engage deeply with business problems through curiosity-driven questioning and brainstorming - Translate experimental results into financial impact and investment recommendations - Analyze marginal and average revenue impacts relative to costs - Communicate complex quantitative ideas clearly to non-technical stakeholders - Demonstrate understanding of Audible's business model and customer experience ABOUT AUDIBLE Audible is the leading producer and provider of audio storytelling. We spark listeners’ imaginations, offering immersive, cinematic experiences full of inspiration and insight to enrich our customers daily lives. We are a global company with an entrepreneurial spirit. We are dreamers and inventors who are passionate about the positive impact Audible can make for our customers and our neighbors. This spirit courses throughout Audible, supporting a culture of creativity and inclusion built on our People Principles and our mission to build more equitable communities in the cities we call home.
Applied Scientist, Prime Video - Content Reasoning, Enrichment and Localization Team
US, WA, Seattle
Prime Video is a first-stop entertainment destination offering customers a vast collection of premium programming in one app available across thousands of devices. Prime members can customize their viewing experience and find their favorite movies, series, documentaries, and live sports – including Amazon MGM Studios-produced series and movies; licensed fan favorites; and programming from Prime Video subscriptions such as Apple TV+, HBO Max, Peacock, Crunchyroll and MGM+. All customers, regardless of whether they have a Prime membership or not, can rent or buy titles via the Prime Video Store, and can enjoy even more content for free with ads. Are you interested in shaping the future of entertainment? Prime Video's technology teams are creating best-in-class digital video experience. As a Prime Video team member, you’ll have end-to-end ownership of the product, user experience, design, and technology required to deliver state-of-the-art experiences for our customers. You’ll get to work on projects that are fast-paced, challenging, and varied. You’ll also be able to experiment with new possibilities, take risks, and collaborate with remarkable people. We’ll look for you to bring your diverse perspectives, ideas, and skill-sets to make Prime Video even better for our customers. With global opportunities for talented technologists, you can decide where a career Prime Video Tech takes you! Key job responsibilities We are looking for passionate, hard-working, and talented individuals to help us push the envelope of content localization. We work on a broad array of research areas and applications, including but not limited to multimodal machine translation, speech synthesis, speech analysis, and asset quality assessment. Candidates should be prepared to help drive innovation in one or more areas of machine learning, audio processing, and natural language understanding. The ideal candidate would have experience in audio processing, natural language understanding and machine learning. Familiarity with machine translation, foundational models, and speech synthesis will be a plus. As an Applied Scientist, you should be a strong communicator, able to describe scientifically rigorous work to business stakeholders of varying levels of technical sophistication. You will closely partner with the solution development teams, and should be intensely curious about how the research is moving the needle for business. Strong inter-personal and mentoring skills to develop applied science talent in the team is another important requirement.
Applied Science Manager, Artificial General Intelligence , Quality Automation
US, WA, Bellevue
The Artificial General Intelligence (AGI) team is seeking a dedicated, skilled, and innovative Applied Science Manager with a robust background in machine learning, statistics, quality assurance, auditing methodologies, and automated evaluation systems to lead a team ensuring the highest standards of data quality, to build industry-leading technology with Large Language Models (LLMs) and multimodal systems. Key job responsibilities As part of the AGI team, an Applied Science Manager will lead and mentor a team of Applied Scientists who develop comprehensive quality strategies and auditing frameworks that safeguard the integrity of data collection workflows. The manager will guide the team in designing auditing strategies with detailed SOPs, quality metrics, and sampling methodologies that align with core scientist team developing Amazon Nova models. The Applied Science Manager will oversee expert-level manual audits, meta-audits to evaluate auditor performance, and provide coaching to uplift overall quality capabilities across the team. The manager will lead research in areas related to HIL data impact to LLM models, and define utility measurement strategies for data generated by AGI-DS for Nova models. The Applied Science Manager will be responsible for recruiting, hiring, and developing team members, conducting performance reviews, setting clear expectations and growth plans, and fostering a culture of scientific excellence and innovation. The manager will communicate with senior leadership, cross-functional technical teams, and customers to collect requirements, describe product features and technical designs, and articulate product strategy. A day in the life An Applied Science Manager with the AGI team will lead quality solution design, guide root cause analysis on data quality issues, drive research into new auditing methodologies, and find innovative ways of optimizing data quality while setting examples for the team on quality assurance best practices and standards. The manager will work closely with talented engineers, domain experts, and vendor teams to put quality strategies and automated judging systems into practice. The manager will also conduct regular 1:1s with team members, provide mentorship and coaching, and ensure the team delivers high-impact results aligned with organizational goals.
Applied Scientist, Grocery, Retail & In-Store Experience (GRAISE)
US, WA, Seattle
The GRAISE team (Grocery, Retail & In-Store Experience) within Worldwide Grocery Store Tech (WWGST) builds foundational AI and machine learning systems that power Amazon's in-store grocery technologies. We develop domain-specific models that solve uniquely complex challenges in grocery — from smart shopping carts and inventory intelligence to personalization and store operations. Our mission is to create technology which makes grocery shopping more convenient, economical, personalized, and enjoyable for customers while empowering retailers with operational efficiency. We are looking for a talented and motivated Applied Scientist to join our team. In this role, you will design, develop, and deploy machine learning and computer vision models and algorithms that solve real-world problems at scale. You will work closely with engineering, product, and business teams to translate ambiguous problems into rigorous scientific solutions, and you will own the end-to-end development of models from ideation through production. This is a high-impact role where your work will directly shape the intelligence layer of Amazon's grocery ecosystem. Key job responsibilities - Design and implement machine learning models to solve complex grocery-domain problems. - Conduct exploratory data analysis and develop deep understanding of domain-specific data challenges. - Collaborate with software engineers to productionize models and ensure reliability at scale. - Define and track key metrics to evaluate model performance and business impact. - Communicate findings and recommendations clearly to technical and non-technical stakeholders. - Stay current with the latest research and evaluate applicability to team problems. - Contribute to a culture of scientific rigor, experimentation, and continuous improvement. A day in the life As an Applied Scientist on the GRAISE team, you'll spend your days analyzing model performance from overnight experiments, collaborating with engineers to deploy computer vision models to production, and prototyping new approaches using multimodal learning with store video and sensor data. You'll present findings to product and business stakeholders, translating technical results into actionable recommendations. Throughout the day, you'll balance rigorous scientific thinking with practical engineering constraints, knowing your work directly improves the shopping experience for millions of customers in Amazon grocery stores.
See more jobs
View from space of a connected network around planet Earth representing the Internet of Things.
Get more from Amazon Science
Subscribe to our monthly newsletter

Amazon.com | Conditions of Use | Privacy | © 1996-2026 Amazon.com, Inc. or its affiliates

Social