search for: rakamaric

Displaying 20 results from an estimated 30 matches for "rakamaric".

2016 Aug 31
2
Publication: "Archer: Effectively Spotting Data Races in Large OpenMP Applications"
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...
2008 Apr 03
3
[LLVMdev] problem with using DSA for a side-effect analysis
...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...
2013 Feb 06
2
[LLVMdev] Adding SMACK to the list of LLVM projects
...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...
2017 Nov 30
2
Publication: Counterexample-Guided Bit-Precision Selection
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 --------------...
2013 Feb 06
0
[LLVMdev] Adding SMACK to the list of LLVM projects
...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...
2014 Apr 01
2
[LLVMdev] LLVM is doing something a bit weird in this example (which messes up DSA)
...(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...
2013 Feb 06
1
[LLVMdev] Adding SMACK to the list of LLVM projects
...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...
2014 Jun 02
3
[LLVMdev] Publication: "SMACK: Decoupling Source Language Details from Verifier Implementations"
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/
2016 Jun 13
3
LLVM APT packages - when will they be back?
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
2014 Dec 15
2
[LLVMdev] Question about node collapse
...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......
2018 Jan 30
0
Publication: Counterexample-Guided Bit-Precision Selection
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...
2008 Apr 03
2
[LLVMdev] problem with using DSA for a side-effect analysis
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
2008 Apr 03
0
[LLVMdev] problem with using DSA for a side-effect analysis
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
2008 Apr 03
1
[LLVMdev] problem with using DSA for a side-effect analysis
...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 > ________________________________...
2008 Apr 04
0
[LLVMdev] problem with using DSA for a side-effect analysis
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...
2015 Aug 19
3
Publication: "Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers"
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
2013 Feb 06
0
[LLVMdev] Adding SMACK to the list of LLVM projects
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...
2014 May 16
2
[LLVMdev] It is possible to somehow turn off coercion of struct parameters into ints?
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
2013 Feb 04
2
[LLVMdev] Adding SMACK to the list of LLVM projects
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
2012 Dec 08
0
[LLVMdev] Status of poolalloc, and in particular DSA
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...