search for: provers

...en to be very scalable in my setting. A nice feature of Spear is that it supports all LLVM integral instructions, including SDIV/UDIV/MUL/..., which makes it really easy to use in combination with LLVM. However, Spear itself is not LLVM-based because many people that are interested in such theorem provers do not use LLVM. Here I provide two simple examples to give you a flavour of Spear: ------------ Example 1 --------------- Assume that you want to generate an instance that corresponds to the following C-like sequential code: int f(int a, int b) { int a1; if (a%2) { a1 = a + 1; }...

On 4/9/07, Domagoj Babic <babic.domagoj at gmail.com> wrote: > > > Traditionally, such analyses have been considered too expensive to be > practical, and were mostly an academic curiosity. The core of the > problem is the lack of adequate automated decision procedures which > could quickly determine whether a set of constraints is satisfiable or > not, and if it is

...ry address has a > counterpart in mathematics. I have tried to simulate memory by arrays in > symbolic execution. But I found it is inadequate. There has been some progress lately (see Rustan Leino's work on the weakest precondition transformer) on handling arrays. Some automated theorem provers even support the theories of arrays (like CVC, Simplify, Yices,...). However, those thm provers do not have a very good support for modular arithmetic. In fact, they most often approximate bounded integers with rationals (reals), and that's one of the reasons why they can't handle operators...

Hello all, thanks for the feedback! It sounds like you are planning to follow the approach of Joshi, Nelson and > Randall ("Denali: A Goal-directed Superoptimizer") in that you don't intend > to exhaustively enumerate all possible code sequences, and see if they are > the same as the original only better; but instead start from the original > code > sequence and

On Thu, 2008-03-27 at 09:51 -0600, John Regehr wrote: > Hey, you need to be careful with this reasoning or else you'll end up > implementing a whole new language, compiler, and OS. > > Oh wait nevermind :). Don't forget prover. :-) shap

...tic of LLVM IR, but it will generate wrong code sequences when lowering to machine code. An example: %3 = fcmp %1, %2 %6 = fcmp %4, %5 %7 = and %3, %6 %8 = and %7, %foo Sometimes you'll be screw if you want to play reassociate %7 and %8. I don't see a easy way of catching them in theorem provers. Haohui On Thu, Apr 7, 2011 at 5:03 PM, Rafael Auler <rafaelauler at gmail.com> wrote: > Hello all, thanks for the feedback! >> >> It sounds like you are planning to follow the approach of Joshi, Nelson >> and >> Randall ("Denali: A Goal-directed Superoptimiz...

...would like to discuss ways of improving other optimization passes similarly (or some examples which have already been implemented). 2. Improve dynamic memory related capabilities of Attributor. For example Improve HeapToStackConversions. Maybe such deductions can help safety (dis)provers. For example, can we improve the use-after-free bug detection using some attributes? 3. Improve Liveness related capabilities of Attributor. Again I want to consider whether some attribute deduction can help liveness (dis)provers. For example NoReturn, WillReturn can be improved. I...

> Don't forget prover. :-) Say on that note here's something that I want to see: a formal semantics for LLVM in for example higher order logic. This would probably not be that difficult. The problem that this solves is that current verified compiler efforts appear to be highly specific to both the language and the target. Once the semantics exists, you can either prove once and

Hi Fahad, > > Improve dynamic memory related capabilities of Attributor. For example > Improve HeapToStackConversions. Maybe such deductions can help safety > (dis)provers. For example, can we improve the use-after-free bug detection > using some attributes? > Stefan should know more about H2S. Regarding the use-after-free, I don't > think there's currently any plans for it directly, but they can be I assume. You are somewhat right. However, H2S is...

Hi, I am brand new to LLVM, or more precisely, trying to be. I'm getting stuck on compiling LLVM. - I tried installing on a Mint 18.1 VM with 6GB RAM, and the builds of some large executables were killed by the OOM killer. I finally realized that I needed to build using shared libraries, and succeeded. This was in November. - I put aside my LLVM project, and just got back to it. I got stuck

Hi, I know there's been some talk about bignums already, this is similar to it, but not exactly the same. I'm currently using LLVM for my master thesis. The goal is to make a compiler for zero-knowledge proofs of knowledge protocols. This compiler should target embedded devices. There's a language called the protocol implementation language in which these protocols should be

Hello, I want to present my project for GSoC 2011 for LLVM below. It would be very nice to hear suggestions and your opinion, thanks! Superoptimization for LLVM IR Objective This project focuses on implementing superoptimization algorithms targeted at the LLVM IR. The project uses arbitrary LLVM bitcode as a training set to discover new peephole optimizations that can be later integrated into

...PM Stefan Stipanovic <stefomeister at gmail.com> > wrote: > >> Hi Fahad, >> >> >>> > Improve dynamic memory related capabilities of Attributor. For example >>> Improve HeapToStackConversions. Maybe such deductions can help safety >>> (dis)provers. For example, can we improve the use-after-free bug >>> detection using some attributes? >>> Stefan should know more about H2S. Regarding the use-after-free, I don't >>> think there's currently any plans for it directly, but they can be I assume. >> >>...

John Regehr wrote: > Say on that note here's something that I want to see: a formal semantics > for LLVM in for example higher order logic. This would probably not be > that difficult. Except that some aspects of the host platform leak through to .bc files. This may or may not be a problem. > Once the semantics exists, you can either prove once and for all the that > each

Hello! With this email we release an extension to OpenSSH that was initially developed as project for our studies at the Univerity of Applied Sciences in Hagenberg. First we would like to describe the purpose of using Zero-Knowledge (ZK) for user authentication. Traditional authentication methods like challenge-response with passwords or public keys leak information about the credentials of

Hi Rafael, don't forget to submit your proposal to GSOC (via the GSOC web-page) - the deadline is today! > > It sounds like you are planning to follow the approach of Joshi, Nelson and > Randall ("Denali: A Goal-directed Superoptimizer") in that you don't intend > to exhaustively enumerate all possible code sequences, and see if they are > the same

Hi, I'd like to link Clang against the STP theorem prover. Since Clang is built by the LLVM build system, I hope this is the correct place to ask for advice. The attached patch allows me to pass `configure` a --with-stp option and provide a path to the install prefix for STP. However, I am not familiar with autoconf, so I am not confident that my changes are the correct way to do this. I

...ding enough > time to understand how to safely inject attributes or _Pragma via > macros) is how to make an assert generate syntax errors when it is > provably violated even in release mode. I like this idea. Sounds good. One can imagine enrolling static analysis and automated theorem provers to help out on the harder problems. :-) > (Am I misreading C99/C0X/C++98/C++0x: does the exact specification of > the expansion of assert in release mode prohibit slipping in a _Pragma > or other implementation-extension constructs to inject flow of control > constraints?) Technica...

Dear all, Is there any project or work about the formal analysis of Xen? For example, Using theorem provers, eg. Acl2, isabelle, coq etc. to verify it. Thanks! Cheers:) Liu Jian -- email to: gjk.liu@gmail.org _______________________________________________ Xen-community mailing list Xen-community@lists.xensource.com http://lists.xensource.com/mailman/listinfo/xen-community

Hi, I'm new to the LLVM mailing list, but I've been working on tools for symbolic execution/formal modeling of LLVM off and on for a while. I’m trying to understand the current status of the LLVM undef/poison semantics from a frontend/verification perspective. I saw there was a lot of interest in a proposed semantics in late 2016 and mid-2017. Perhaps this was due to the “Taming