Skip to main content
  • Log in
  • Manage Cookies
Eclipse Plugins, Bundles and Products - Eclipse Marketplace
  • My Marketplace
  • Add Content
  • More

      • Community

      • Marketplace
      • Events
      • Planet Eclipse
      • Newsletter
      • Videos
      • Blogs

      • Participate

      • Report a Bug
      • Forums
      • Mailing Lists
      • Wiki
      • IRC
      • Research

      • Eclipse IDE

      • Download
      • Learn More
      • Documentation
      • Getting Started / Support
      • How to Contribute
      • IDE and Tools
      • Newcomer Forum

    • Search

  1. Home
  2. Marketplace
  3. Tools
  4. Kopitiam

Please be aware that some listings have been temporarily delisted from our marketplace in order to improve the security of the platform. We apologize for any inconvenience this may caused.

For more information on this matter, please visit #1.

If you are a listing owner and would like to have your listing(s) reinstated, please open a ticket at https://gitlab.eclipse.org/eclipsefdn/it/websites/marketplace.eclipse.org/-/issues.

Thank you for your understanding and cooperation.

Kopitiam

Kopitiam
3
0
Install

Drag to Install!

Drag to your running Eclipse* workspace.
*Requires Eclipse Marketplace Client

Add this URL to your Eclipse Installation to reach this solution's update site.

Mars (4.5)
Luna (4.4)
Kepler (4.3)
Juno (4.2, 3.8)
Previous to Juno (<=4.1)
Neon (4.6)
Oxygen (4.7)
Photon (4.8)
2018-09 (4.9)

https://www.itu.dk/research/tomeso/kopitiam/eclipse
Learn more...

Screenshot 0

Details Group Tabs

Details

Kopitiam is an Eclipse plugin for certifying full functional
correctness of Java programs using a higher-order separation
logic. Kopitiam extends the Java IDE with an interactive environment
for program verification, powered by the general-purpose proof
assistant Coq. Moreover, Kopitiam includes a feature-complete
development environment for Coq theories, where users can define
program models, and prove theorems required for the program
verification.

Categories:
  • Other
Tags:
  • specification,
  • coq,
  • proof,
  • separation logic
Additional Details
Eclipse Versions: 
Mars (4.5), Luna (4.4), Kepler (4.3), Juno (4.2, 3.8), Previous to Juno (<=4.1), Neon (4.6), Oxygen (4.7), Photon (4.8), 2018-09 (4.9)
Platform Support: 
Windows, Mac, Linux/GTK
Organization Name: 
IT University of Copenhagen
Development Status: 
Beta
Date Created: 
Wed, 2012-08-15 11:47
License: 
BSD
Date Updated: 
Wed, 2022-12-14 09:48
Submitted by: 
Hannes Mehnert
Screenshots
Screenshot 0
Metrics
DateRankingInstallsClickthroughs
March 2023NA0 (0%)7
February 2023NA0 (0%)10
January 2023NA0 (0%)8
December 2022NA0 (0%)11
November 2022NA0 (0%)7
October 2022NA0 (0%)3
September 2022NA0 (0%)3
August 2022NA0 (0%)7
July 2022790/8161 (0%)7
June 2022NA0 (0%)9
May 2022NA0 (0%)6
April 2022NA0 (0%)9
View Data for all Listings
Errors

Unsuccessful Installs in the last 7 Days: 0

Download last 500 errors (CSV)
External Install Button

Marketplace Drag to Install button

By adding the following code below to your website you will be able to add an install button for Kopitiam.

HTML Code:


Markdown Syntax:



Output: Drag to your running Eclipse* workspace. *Requires Eclipse Marketplace Client
Wednesday, March 29, 2023 - 12:05
  • Sign in to post reviews.

Markets

  • Eclipse Project (4)
  • Tools (1342)
    • Application Development Frameworks (171)
    • Application Management (32)
    • Application Server (31)
    • BIRT (10)
    • Build and Deploy (104)
    • Business Intelligence, Reporting and Charting (14)
    • Code Management (117)
    • Collaboration (37)
    • Database (44)
    • Database Development (34)
    • Database Persistence (17)
    • Documentation (60)
    • Eclipse Kura (122)
    • Eclipse SmartHome (46)
    • EclipseRT Target Platform Components (10)
    • Editor (339)
    • Entertainment (14)
    • General Purpose Tools (124)
    • Graphics (34)
    • IDE (344)
    • Internet of Things (IoT) (35)
    • J2EE Development Platform (44)
    • J2ME (5)
    • Languages (155)
    • Linux Tools (19)
    • Logging (22)
    • Mobile and Device Development (49)
    • Modeling (90)
    • Modeling Tools (146)
    • Mylyn Connectors (20)
    • Network (14)
    • Other (74)
    • Process (18)
    • Profiling (22)
    • Programming Languages (100)
    • Reporting (32)
    • Rich Client Applications (39)
    • Science (4)
    • SCM (20)
    • Search (42)
    • SOA Development (15)
    • Source Code Analyzer (99)
    • Systems Development (59)
    • Team Development (54)
    • Testing (90)
    • Tools (568)
    • UI (97)
    • UML (40)
    • Web (90)
    • Web Services (31)
    • Web, XML, Java EE and OSGi Enterprise Development (32)
    • XML (29)
  • IoT (172)
    • Eclipse Kura (122)
    • Eclipse SmartHome (46)
  • RCP Applications (79)
  • Training & Consulting (53)
  • Long Term Support (11)

Search

Advanced Search

More like this

  • Autodetect Encoding
  • CombiS-BP Editor
  • Arden4Eclipse
  • IBM WebSphere Application Server Migration Toolkit- Competitive Tools
  • C4J- Contracts for Java

Favorited by

Eclipse Foundation

  • About Us
  • Contact Us
  • Sponsor
  • Members
  • Governance
  • Code of Conduct
  • Logo and Artwork
  • Board of Directors
  • Careers

Legal

  • Publishing Guidelines
  • Privacy Policy
  • Terms of Use
  • Copyright Agent
  • Eclipse Public License
  • Legal Resources

Useful Links

  • Welcome to Marketplace
  • Report a Bug
  • Documentation
  • How to Contribute
  • Mailing Lists
  • Forums
  • Marketplace

Other

  • IDE and Tools
  • Projects
  • Working Groups
  • Research@Eclipse
  • Report a Vulnerability
  • Service Status

Copyright © Eclipse Foundation. All Rights Reserved.

Back to the top