search for: soarlab

Hi, So, SMACK is a software verifier based around LLVM, and you can find more info (PDF, title, abstract) about our recent publication here: http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/ I would appreciate if you could add it to your list of LLVM-based publications. Thanks! Best, -- Zvonimir -- http://zvonimir.info http://soarlab.org/

...tomicCmpXchgInst does not return a pointer type, nothing gets merged. And in the example I posted, a pointer value is indeed not returned (but rather an i64 value "masking" an i32* value). And so DSA does not do the right thing in this case... -- Zvonimir -- http://zvonimir.info http://soarlab.org/ On Mon, Mar 31, 2014 at 10:29 PM, John Criswell <criswell at illinois.edu> wrote: > On 3/31/14, 6:09 PM, Zvonimir Rakamaric wrote: >> >> Hi all, >> >> I have yet another DSA-related question :), and I would appreciate >> your help. Actually, the followi...

Hi, We recently published another paper that leverages LLVM (through our SMACK software verifier and novel tool called Whoop), and this time we focus on detecting concurrency bugs in device drivers: http://soarlab.org/2015/08/ase2015-ddr/ You can find all the required info (PDF, title, abstract, etc.) at the above webpage. I would appreciate if you could add this paper to your list of LLVM-based publications. Thanks! Best, -- Zvonimir -------------- next part -------------- An HTML attachment was scrubbe...

Hi, We just published our work that uses LLVM for software verification: Counterexample-Guided Bit-Precision Selection Shaobo He, Zvonimir Rakamaric Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS), November 2017. Link: http://soarlab.org/2017/09/aplas2017-hr/ I would appreciate if someone could add it to your publication list. Thanks! -- Zvonimir -- http://zvonimir.info http://soarlab.org -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/2...

Thanks John! You would not believe this :), but literally just 5 minutes ago I saw the TypeSafety pass and it seems to be exactly what we need. So we'll try to leverage that... Best, -- Zvonimir -- http://zvonimir.info http://soarlab.org/ On Mon, Dec 15, 2014 at 10:28 AM, John Criswell <jtcriswel at gmail.com> wrote: > On 12/14/14, 4:33 PM, Zvonimir Rakamaric wrote: >> >> Hi John, all, >> >> Thanks for your responses everybody. >> >> This is actually helpful and I think I now bette...

...ed fine, then we have a problem with DSA when it gets to this cmpxchg instruction since DSA then does not know that the second and third arguments to cmpxchg are in fact pointers. Messy stuff... Your help would be greatly appreciated... Thanks! Cheers, -- Zvonimir -- http://zvonimir.info http://soarlab.org/

...ening on the node. Am I getting this about right? If you have time to point us at some API functions to get us started with the above idea, that would be great. If not, then don't worry, hopefully we'll figure it out on our own. Thanks! Best, -- Zvonimir -- http://zvonimir.info http://soarlab.org/ On Sun, Dec 14, 2014 at 10:11 AM, John Criswell <jtcriswel at gmail.com> wrote: > On 12/12/14, 8:14 PM, Shaobo wrote: >> >> Hi guys, >> >> I'm working on a project using DSA to mark the type-unsafe store >> operations. The example code is below, &gt...

...) to the list. Thanks, -- Zvonimir On Tue, Jun 21, 2016 at 12:07 PM Zvonimir Rakamaric <zvonimir at cs.utah.edu> wrote: > Hi, > > We recently published a paper that leverages clang/LLVM (through > ThreadSanitizer) to dynamically detect data races in OpenMP programs: > http://soarlab.org/2016/02/ipdps2016-agralslpm/ > > You can find all the required info (PDF, title, abstract, etc.) at the > above webpage. > > I would appreciate if you could add this paper to your list of LLVM-based > publications. > > Thanks! > > Best, > -- Zvonimir > ------...

On 11/29/17 7:42 PM, Zvonimir Rakamaric via llvm-dev wrote: > Counterexample-Guided Bit-Precision Selection I've added this publication to the publication list. Please let me know if I need to make any corrections. Regards, John Criswell -- John Criswell Assistant Professor Department of Computer Science, University of Rochester http://www.cs.rochester.edu/u/criswell

In particular, I would for example like to prevent that two fields of type i32 are packed into an i64 parameter. And so on... Thanks! -- Zvonimir

Hi guys, I'm working on a project using DSA to mark the type-unsafe store operations. The example code is below, > int main() { > int *a = (int*)malloc(sizeof(int)); > > *a = 256; > *((char *)a) = 1; > assert(*a == 257); > > free(a); > > return 0; > } Based on my understanding of DSA, *((char *)a) = 1 will cause the node to which "a"

Hello, all, My name is Scott Santucci and I'm a software developer kicking around various wild ideas. (I wish I had something more interesting to say about myself than that, but nothing comes to mind; my day job is in SQL and Java, nothing to do with LLVM.) I am wondering whether anyone has tried using LLVM to apply formal verification to program code. I'm thinking about trying to