search for: rakamaric

Hi, Coming back to this, I would greatly appreciate if someone could add this publication (based on TSan) 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 (P...

...erface. > > > > --Vikram > > http://www.cs.uiuc.edu/~vadve > > http://llvm.org/ > > > > > > > > > > > > On Apr 3, 2008, at 12:45 PM, Andrew Lenharth wrote: > > > > > On Thu, Apr 3, 2008 at 12:29 PM, Zvonimir Rakamaric <zrakamar at gmail.com > > > > wrote: > > >> Currently I am using DSGraph::computeNodeMapping to do the task, > > >> but I > > >> am not sure if that's the way to go.... > > > > > > I believe that is the correct fu...

...6, 2013 at 1:10 AM, Bill Wendling <wendling at apple.com> wrote: > Hi Zvonimir, > > We normally list projects that use LLVM when we do a release. The next release will be 3.3, which will probably start up in 5 months or so. > > -bw > > On Feb 3, 2013, at 9:16 PM, Zvonimir Rakamaric <zvonimir at cs.utah.edu> wrote: > >> Hi guys, >> >> So, I've been a long-term user of LLVM, and currently me and my >> students are actively using LLVM in several projects of ours. >> >> At this point, I would greatly appreciate if you could add SMA...

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

...add the URL to the User's page. Is the Github URL what you want to use, or is there a web page with more information that we should link to instead? -- John T. ________________________________________ From: llvmdev-bounces at cs.uiuc.edu [llvmdev-bounces at cs.uiuc.edu] on behalf of Zvonimir Rakamaric [zvonimir at cs.utah.edu] Sent: Wednesday, February 06, 2013 9:10 AM To: Bill Wendling Cc: LLVM Developers Mailing List Subject: Re: [LLVMdev] Adding SMACK to the list of LLVM projects Thanks Bill! So should I email you again in 5 months? -- http://www.zvonimir.info On Wed, Feb 6, 2013 at 1:10...

...(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 following example generates some interesting >> potential issues in the LLVM IR too. >> >> Here is the example in C: >> #de...

...User's page. Is the Github URL what you want to use, or is there a web page with more information that we should link to instead? > > -- John T. > ________________________________________ > From: llvmdev-bounces at cs.uiuc.edu [llvmdev-bounces at cs.uiuc.edu] on behalf of Zvonimir Rakamaric [zvonimir at cs.utah.edu] > Sent: Wednesday, February 06, 2013 9:10 AM > To: Bill Wendling > Cc: LLVM Developers Mailing List > Subject: Re: [LLVMdev] Adding SMACK to the list of LLVM projects > > Thanks Bill! So should I email you again in 5 months? > > -- > http://www...

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/

Hi, Our tool SMACK (https://github.com/smackers/smack/) relies on installing LLMV from APT packages that used to be provided here: http://llvm.org/apt/ This link has been down for several weeks at this point (I think). Do you have a rough estimate for when you will bring this back? Our users are having trouble installing SMACK due to the above problem, and so I am wondering if we should look

...tes 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 better understand what is >> going on here. Unless there is a pointer involved, DSA will not >> collapse nodes. That makes sense......

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

Hi, I am using DSA in the project I am working on. Currently, I am working on automatic inference of function frame conditions to be used in the modular verification tool for C I am developing. Here is a part of my algorithm I am not exactly sure how to do: Let's say function foo calls function bar, and they have corresponding DSGraphs DSG_foo and DSG_bar. Function bar modifies some memory

On Thu, Apr 3, 2008 at 12:29 PM, Zvonimir Rakamaric <zrakamar at gmail.com> wrote: > Currently I am using DSGraph::computeNodeMapping to do the task, but I > am not sure if that's the way to go.... I believe that is the correct function to use. Andrew

...sentially that, although perhaps he needs it as DS nodes explicitly rather than via the generic queries in the AliasAnalysis interface. --Vikram http://www.cs.uiuc.edu/~vadve http://llvm.org/ On Apr 3, 2008, at 12:45 PM, Andrew Lenharth wrote: > On Thu, Apr 3, 2008 at 12:29 PM, Zvonimir Rakamaric <zrakamar at gmail.com > > wrote: >> Currently I am using DSGraph::computeNodeMapping to do the task, >> but I >> am not sure if that's the way to go.... > > I believe that is the correct function to use. > > Andrew > ________________________________...

On Thu, Apr 3, 2008 at 4:53 PM, Zvonimir Rakamaric <zrakamar at gmail.com> wrote: > Thanks guys! > > I was looking into ModRef before, but I don't think that's exactly > what I need. ModRef API call getModRefInfo requires a Value to be > passed to it. However, some memory location M (which is a <DSNode, > offs...

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

Hi Zvonimir, We normally list projects that use LLVM when we do a release. The next release will be 3.3, which will probably start up in 5 months or so. -bw On Feb 3, 2013, at 9:16 PM, Zvonimir Rakamaric <zvonimir at cs.utah.edu> wrote: > Hi guys, > > So, I've been a long-term user of LLVM, and currently me and my > students are actively using LLVM in several projects of ours. > > At this point, I would greatly appreciate if you could add SMACK > static checker, wh...

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, So, I've been a long-term user of LLVM, and currently me and my students are actively using LLVM in several projects of ours. At this point, I would greatly appreciate if you could add SMACK static checker, which relies on LLVM, to the list of LLVM projects. SMACK is an open-source static checker built on top of LLVM, and we are hoping to get more collaborators and contributors this

On 12/6/12 4:47 PM, Zvonimir Rakamaric wrote: > Hi all, > > I've been using LLVM in my software analysis projects for quite a few > years now, and several years back I relied on results of DSA analysis > in my SMACK tool for checking C programs. > > At some point that part of SMACK got deprecated, but now I woul...