Skip to main content

9 Result(s)

within Nuno P. Lopes Remove this filter

and

  1. Chapter and Conference Paper

    An SMT Encoding of LLVM’s Memory Model for Bounded Translation Validation

    Several automatic verification tools have been recently developed to verify subsets of LLVM’s optimizations. However, none of these tools has robust support to verify memory optimizations.

    Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur, Nuno P. Lopes in Computer Aided Verification (2021)

    Download PDF (918 KB) View Chapter

  2. No Access

    Chapter and Conference Paper

    Supercharging Plant Configurations Using Z3

    We describe our experiences using Z3 for synthesizing and optimizing next generation plant configurations for a car manufacturing company (The views expressed in this writing are our own. They make no represen...

    Nikolaj Bjørner, Maxwell Levatich… in Integration of Constraint Programming, Art… (2021)

  3. Chapter and Conference Paper

    AliveInLean: A Verified LLVM Peephole Optimization Verifier

    Ensuring that compiler optimizations are correct...

    Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes in Computer Aided Verification (2019)

    Download PDF (413 KB) View Chapter

  4. No Access

    Chapter and Conference Paper

    Fast BGP Simulation of Large Datacenters

    Frequent configuration churn caused by maintenance, upgrades, hardware and firmware failures regularly leads to costly outages. Preventing network outages caused by misconfigurations is important for ensuring ...

    Nuno P. Lopes, Andrey Rybalchenko in Verification, Model Checking, and Abstract… (2019)

  5. No Access

    Article

    Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic

    Proving equivalence of programs has several important applications, including algorithm recognition, regression checking, compiler optimization verification and validation, and information flow checking. Despi...

    Nuno P. Lopes, José Monteiro in International Journal on Software Tools fo… (2016)

  6. No Access

    Chapter and Conference Paper

    Weakest Precondition Synthesis for Compiler Optimizations

    Compiler optimizations play an increasingly important role in code generation. This is especially true with the advent of resourcelimited mobile devices. We rely on compiler optimizations to improve performanc...

    Nuno P. Lopes, José Monteiro in Verification, Model Checking, and Abstract Interpretation (2014)

  7. No Access

    Chapter and Conference Paper

    Automatic Equivalence Checking of UF+IA Programs

    Proving the equivalence of programs has several important applications, including algorithm recognition, regression checking, compiler optimization verification, and information flow checking.

    Nuno P. Lopes, José Monteiro in Model Checking Software (2013)

  8. Chapter and Conference Paper

    HSF(C): A Software Verifier Based on Horn Clauses

    HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use...

    Sergey Grebenshchikov, Ashutosh Gupta… in Tools and Algorithms for the Construction … (2012)

    Download PDF (85 KB)

  9. No Access

    Chapter and Conference Paper

    Distributed and Predictable Software Model Checking

    We present a predicate abstraction and refinement-based algorithm for software verification that is designed for the distributed execution on compute nodes that communicate via message passing, as found in tod...

    Nuno P. Lopes, Andrey Rybalchenko in Verification, Model Checking, and Abstract… (2011)