search for: prover

...n 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 satisfiable, find a solution. Recently, I've released Spear -- automated modular arithmetic theorem prover, which has proven 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...

...d a solution. I think the real difficult thing in path sensitive program analysis (or symbolic execution) is not the lack of decision procedures, but the translation of arbitrary pointer operations and library function calls in C/C++ program into the mathematics supported by the automated theorem prover. Almost every concept in the computer program except memory address has a counterpart in mathematics. I have tried to simulate memory by arrays in symbolic execution. But I found it is inadequate. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm....

...ink the real difficult thing in path sensitive program analysis (or > symbolic execution) is not the lack of decision procedures, but the > translation of arbitrary pointer operations and library function calls in > C/C++ program into the mathematics supported by the automated theorem > prover. > Almost every concept in the computer program except memory 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 precon...

...inal. Is that right? > > Exactly. If we can use axioms/transformations/identities which don't modify the code behavior, but just tries to interpret instruction semantics in a different way, so as to find another (and hopefully simpler) instructions to do the same job, the role of the SAT prover is no longer necessary, since the search space is constrained to expressions which are semantically equivalent. Example: Transformation: (ADD Operand_A, Contant 0) <- equivalent to-> Operand_A Using this transformation, the search algorithm now can simplify "add A with 0" to &q...

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 Superoptimi...

...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...

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 i...

...ence to `llvm::DisableABIBreakingChecks' This discussion, from this mailing list, points out that I need to build LLVM with -DLLVM_DISABLE_ABI_BREAKING_CHECKS_ENFORCING=OFF. - So now I am trying to rebuild LLVM, and ran into a few new problems. First, I discovered that I need the Z3 theorem prover. Unsure why this problem did not show up before. Second, I'm running into many errors like this: CMake Error at cmake/modules/AddLLVM.cmake:570 (target_link_libraries): Attempt to add link library "clangAST" to target "clangApplyReplacements" which is not b...

...rget embedded devices. There's a language called the protocol implementation language in which these protocols should be implemented. Here's an excerpt from a simple sample of it: Common ( Z SZKParameter = 80; Prime(1024) p = 17; Prime(160) q = 1; Zmod*(p) y = 1, g=3 ) { } Prover(Zmod+(q) x) { Zmod+(q) _s_1=1, _r_1=4; Def (Void): Round0(Void) { } Def (Zmod*(p) _t_1): Round1(Void) { _r_1 := Random(Zmod+(q)); _t_1 := (g^_r_1); } Def (_s_1): Round2(_C=Int(80) _c) { _s_1 := (_r_1+(x*_c));...

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. >> >&gt...

...folks on this idea (they have a formal > semantics for an ARM ISA, for example) but so far no dice. You could sell it to me. How much money do you have? ;-) But seriously, that is something I would very much like to see. One of the reasons why you have not had success may be that with current prover technology, formalizing LLVM semantics and carrying out proofs would be a fairly straightforward exercise, but not a trivial amount of work. Not a good combination in academic sense. On the other hand, formalizing LLVM and proving some properties would make for a very nice open source proof projec...

...tudies 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 a user (prover) to the verifying or any other party that can access the exchanged messages. Thus, with every finished authentication process the adversary has a greater chance of successfully purporting to third parties to be the prover. ZK avoids this drawback. The theory is more than twenty years old and is...

...? > > > Exactly. If we can use axioms/transformations/identities which don't modify the > code behavior, but just tries to interpret instruction semantics in a different > way, so as to find another (and hopefully simpler) instructions to do the same > job, the role of the SAT prover is no longer necessary, since the search space > is constrained to expressions which are semantically equivalent. > > Example: > Transformation: (ADD Operand_A, Contant 0) <- equivalent to-> Operand_A > > Using this transformation, the search algorithm now can simplify &qu...

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...

...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?) Technic...

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

...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 Undefined..." PLDI paper, which seemed like a nice writeup. I'd like to formalize this in a theorem prover or Cryptol. Since the mid 2017 discussion, is there an emerging consensus of the semantics of undef/poison? If so, is there a newer writeup than the PLDI paper? The paper semantics in Section 4 on bitvector types "isz” seem reasonable to me. However, I was surprised by the pointer semantic...