[Haskell] RV 2017 - Last Call for Participation

[Ayoub Nouri]

LAST CALL FOR PARTICIPATION


RV’17 - RUNTIME VERIFICATION 2017


The 17th International Conference on Runtime Verification

September 13-16 2017, Seattle, WA, USA


Website: http://rv2017.cs.manchester.ac.uk 



Program: http://easychair.org/smart-program/RV2017/

RV-CuBES Program: http://easychair.org/smart-program/RV-CuBES2017/


Affiliated Event:


 RV-CuBES - An International Workshop on Competitions, Usability,

 Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools


=== OVERVIEW ===


Runtime verification is concerned with the monitoring and analysis of

the runtime behaviour of software and hardware systems. Runtime

verification techniques are crucial for system correctness, reliability,

and robustness; they provide an additional level of rigor and

effectiveness compared to conventional testing, and are generally more

practical than exhaustive formal verification. Runtime verification can

be used prior to deployment, for testing, verification, and debugging

purposes, and after deployment for ensuring reliability, safety, and

security and for providing fault containment and recovery as well as

online system repair. Topics of interest to the conference include:


   specification languages

   monitor construction techniques

   program instrumentation

   logging, recording, and replay

   combination of static and dynamic analysis

   specification mining and machine learning over runtime traces

   monitoring techniques for concurrent and distributed systems

   runtime checking of privacy and security policies

   statistical model checking

   metrics and statistical information gathering

   program/system execution visualization

   fault localization, containment, recovery and repair

   integrated vehicle health management (IVHM)


Application areas of runtime verification include cyber-physical

systems, safety/mission-critical systems, enterprise and systems

software, autonomous and reactive control systems, health management and

diagnosis systems, and system security and privacy.


=== INVITED TALKS ===


Rodrigo Fonseca, Brown University, USA:


   “The Design and Applications for a Tracing Plane for Distributed 
Systems”



Vlad Levin and Jakob Lichtenberg, Microsoft, USA:


   “Windows Driver Verification Platform”


Andreas Zeller, Saarland University, Germany:


   “Learning Input Languages for Runtime Verification”


=== TUTORIALS ===


Ankush Desai and Shaz Qadeer, UC Berkeley and Microsoft Research, USA:


   “P : Modular and Safe Asynchronous Programming”


Madhusudan Parthasarathy, University of Illinois at Urbana-Champaign, USA:


   “Machine-learning State Properties”


Adrian Francalanza, University of Malta, Malta:


   “Foundations For Runtime Monitoring”


=== VENUE ===


The 17th International Conference on Runtime Verification will be held

in the Sheraton Seattle Hotel situated in downtown Seattle. The venue is

within walking distance of the famous Pike Place Market, Seattle Art

Museum, Seattle Aquarium, and the Historic Seattle Waterfront. The

weather in September still permits many open-air opportunities to shop,

eat, and even sail in the Elliott Bay. Exceptionally well organized,

Seattle’s public transport connects the conference venue with the

Seattle Center, which is the home of popular attractions like the Space

Needle, EMP Museum, and Chihuly Garden and Glass.


=== REGISTRATION ===


Registration is available using the web-based registration form,

with online payment on a secure website. Please use one form per

attendee.


Different possibilities of registration are available:


Tutorial Day Only (13th September): 210 USD


Conference including tutorial day and RV-CuBES (13-16th September)

   Full Registration: 780 USD

   Student Registration: 580 USD


=== Program Committee ===


Wolfgang Ahrendt, Chalmers Univ. of Technology/Univ. of Gothenburg, Sweden

Cyrille Artho, KTH Royal Institute of Technology, Sweden

Howard Barringer,The University of Manchester, UK

Ezio Bartocci,Vienna University of Technology, Austria

Andreas Bauer,KUKA Systems, Germany

Saddek Bensalem,VERIMAG (University of Grenoble Alpes), France

Eric Bodden, Paderborn University / Fraunhofer IEM, Germany

Borzoo Bonakdarpour, McMaster University, Canada

Christian Colombo,University of Malta, Malta

Ylies Falcone,University of Grenoble Alpes, France

Grigory Fedyukovich,University of Washington, USA

Lu Feng,University of Virginia, USA

Patrice Godefroid,Microsoft Research, USA

Jean Goubault-Larrecq,CNRS & ENS de Cachan, France

Alex Groce,Northern Arizona University, USA

Radu Grosu,Vienna University of Technology, Austria

Sylvain Hallé,University of Québec at Chicoutimi, Canada

Marieke Huisman, University of Twente, Netherlands

Franjo Ivancic,Google, USA

Bengt Jonsson,Uppsala University, Sweden

Felix Klaedtke,NEC Europe Ltd.

Rahul Kumar,Microsoft Research, USA

Kim Larsen,Aalborg 

Re: [Haskell] [Haskell-beginners] Restrict type in phantom data-type

[Baa]

David, hello!

1. Is it the same/different as:

  data family Day a
  data Sunny
  data Rainy
  data instance Day Sunny = SunnyDay deriving Show
  data instance Day Rainy = RainyDay deriving Show

  ..and here you can not create `Day Int` object because no `Day Int`
  constructor (but you can create such constructor)

? Or in case with type families there is possibility to extend it to
`Day Int` and in case with DayaKinds it's totally impossible?

2. I read somewhere (on forums) that restrictions on data types... I
don't remember exactly, but something like they are not real
restrictions or are related to old extension which is/will be
deprecated. I'm not sure. Also, I'm not sure is it - in your example -
restriction (constraint) or something else. Am I wrong?

> This is maybe edging toward haskell-cafe territory, but you can
> definitely do this in haskell.
> 
> {-# LANGUAGE DataKinds, KindSignatures #-}
> 
> data DayType = Sunny | Rainy
> 
> data Day (a :: DayType) = Day
> 
> 
> sunnyDay :: Day Sunny
> sunnyDay = Day
> 
> rainyDay :: Day Rainy
> rainyDay = Day
> 
> -- impossibleDay :: Day ()
> -- impossibleDay = Day
> 
> On Fri, Sep 1, 2017 at 10:18 AM, Baa  wrote:
> > Hello, List!
> >
> > For example, I have specialized (right nameis phantom?) type:
> >
> >   data Day a = Day { ... no `a` here }
> >   data Sunny
> >   data Rainy
> >
> >   joyToday :: Day Sunny -> IO ()
> >   joyToday day = ...
> >
> >   melancholyToday :: Day Rainy -> IO ()
> >   melancholyToday day = ...
> >
> > And I can create (in spite of that it's phantom) some day:
> >
> >   let day1 = Day {...} :: Day Sunny
> >   joyToday day1
> >
> > but no problem to create `Day Int`, `Day Char`, etc which is
> > pointless actually (sure "creator"-function can be exported from the
> > module only, but I'm talking about type-level solution).
> >
> > I know that constraints (`... =>`) on data types are
> > redundant/removed from the language. And I'm not sure how it's
> > possible to restrict that parameter `a` (I know that it's possible
> > to Java/C++/Perl6 (not sure), some other languages but how to add
> > such restriction in Haskell? IMHO type families can help but I'm
> > not sure how it will look (Sunny, Rainy are "nullary" type, so...).
> >
> > Is it possible for Haskell too?
> >
> > ===
> > Best regards, Paul
> > ___
> > Beginners mailing list
> > beginn...@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners  
> ___
> Beginners mailing list
> beginn...@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

___
Haskell mailing list
Haskell@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell

Re: [Haskell] [Haskell-beginners] Restrict type in phantom data-type

[David Feuer]

This is off-topic for this list. This list is for announcements. This
belongs on haskell-c...@haskell.org

On Sep 1, 2017 11:05 AM, "Baa"  wrote:

> David, hello!
>
> 1. Is it the same/different as:
>
>   data family Day a
>   data Sunny
>   data Rainy
>   data instance Day Sunny = SunnyDay deriving Show
>   data instance Day Rainy = RainyDay deriving Show
>
>   ..and here you can not create `Day Int` object because no `Day Int`
>   constructor (but you can create such constructor)
>
> ? Or in case with type families there is possibility to extend it to
> `Day Int` and in case with DayaKinds it's totally impossible?
>
> 2. I read somewhere (on forums) that restrictions on data types... I
> don't remember exactly, but something like they are not real
> restrictions or are related to old extension which is/will be
> deprecated. I'm not sure. Also, I'm not sure is it - in your example -
> restriction (constraint) or something else. Am I wrong?
>
> > This is maybe edging toward haskell-cafe territory, but you can
> > definitely do this in haskell.
> >
> > {-# LANGUAGE DataKinds, KindSignatures #-}
> >
> > data DayType = Sunny | Rainy
> >
> > data Day (a :: DayType) = Day
> >
> >
> > sunnyDay :: Day Sunny
> > sunnyDay = Day
> >
> > rainyDay :: Day Rainy
> > rainyDay = Day
> >
> > -- impossibleDay :: Day ()
> > -- impossibleDay = Day
> >
> > On Fri, Sep 1, 2017 at 10:18 AM, Baa  wrote:
> > > Hello, List!
> > >
> > > For example, I have specialized (right nameis phantom?) type:
> > >
> > >   data Day a = Day { ... no `a` here }
> > >   data Sunny
> > >   data Rainy
> > >
> > >   joyToday :: Day Sunny -> IO ()
> > >   joyToday day = ...
> > >
> > >   melancholyToday :: Day Rainy -> IO ()
> > >   melancholyToday day = ...
> > >
> > > And I can create (in spite of that it's phantom) some day:
> > >
> > >   let day1 = Day {...} :: Day Sunny
> > >   joyToday day1
> > >
> > > but no problem to create `Day Int`, `Day Char`, etc which is
> > > pointless actually (sure "creator"-function can be exported from the
> > > module only, but I'm talking about type-level solution).
> > >
> > > I know that constraints (`... =>`) on data types are
> > > redundant/removed from the language. And I'm not sure how it's
> > > possible to restrict that parameter `a` (I know that it's possible
> > > to Java/C++/Perl6 (not sure), some other languages but how to add
> > > such restriction in Haskell? IMHO type families can help but I'm
> > > not sure how it will look (Sunny, Rainy are "nullary" type, so...).
> > >
> > > Is it possible for Haskell too?
> > >
> > > ===
> > > Best regards, Paul
> > > ___
> > > Beginners mailing list
> > > beginn...@haskell.org
> > > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
> > ___
> > Beginners mailing list
> > beginn...@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
> ___
> Haskell mailing list
> Haskell@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
>
___
Haskell mailing list
Haskell@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell

Re: How to get a heap visualization

[Joachim Breitner]

Hi,

author of ghc-heap-view here.

Am Mittwoch, den 30.08.2017, 18:34 +0300 schrieb Yitzchak Gale:
> Getting ghc-vis to compile looks hopeless, for a number of reasons.
> The dependencies on gtk and cairo are huge.

Is that really a problem?

>  It hasn't been updated
> on Hackage for a year and a half. It requires base < 4.9.

GitHub is already ahead. I guess this just needs to be uploaded?
https://github.com/def-/ghc-vis/blob/master/ghc-vis.cabal


> I need to run
> the visualizer either on a headless Ubuntu 16.04 server, or locally on
> Windows.

Ok, that is more tricky.

> The heap scraper backend for ghc-vis, ghc-heap-view, looks usable,
> and better supported than vacuum. But is there a quick and simple
> visualizer for its output, without ghc-vis?


Well, the :printHeap command that comes with it does “visualize” things
as something resembling Haskell syntax:

let x1 = "A Value"
x16 = True : False : x16
in (x1,x1,x16)

I don’t know of anything more graphical besides ghc-vis, but you could
roll your own, if you want to; you can use ghc-heap-view to get a graph
using
http://hackage.haskell.org/package/ghc-heap-view-0.5.9/docs/GHC-HeapView.html#v:buildHeapGraph
and then visualize that as you like.

Greetings,
Joachim

-- 
Joachim “nomeata” Breitner
  m...@joachim-breitner.de
  https://www.joachim-breitner.de/


signature.asc
Description: This is a digitally signed message part
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users